Refine abstraction in hyps for with nodes in proof

mattam82 · Nov 21, 2017 · 08df324 · 08df324
1 parent 37b6e9c
commit 08df324
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 3 deletions.
diff --git a/src/equations_common.ml b/src/equations_common.ml
@@ -801,6 +801,8 @@ let observe s tac =
                             | Refiner.FailError (n,expl) ->
                                (str" Fail error " ++ int n ++ str " for " ++ str s ++ spc () ++ Lazy.force expl ++
                                   str " on " ++ Printer.pr_goal gls)
+                            | Pretype_errors.PretypeError (env, sigma, e) ->
+                               (str " Pretype error: " ++ Himsg.explain_pretype_error env sigma e)
                             | _ -> CErrors.iprint iexn));
                    Proofview.tclUNIT ())) gls
 

diff --git a/src/principles_proofs.ml b/src/principles_proofs.ml
@@ -270,6 +270,10 @@ let change_in_app f args idx arg =
   args'.(idx) <- arg;
   mkApp (f, args')
 
+let hyps_after sigma pos args =
+  let args' = Array.sub args (pos + 1) (Array.length args - (pos + 1)) in
+  Array.fold_right (fun c acc -> ids_of_constr ~all:true sigma acc c) args' Id.Set.empty
+
 let rec aux_ind_fun info chop unfs unfids = function
   | Split ((ctx,pats,_), var, _, splits) ->
      let unfs =
@@ -317,15 +321,17 @@ let rec aux_ind_fun info chop unfs unfids = function
          let f, fargs = destApp (project gl) last_arg.(0) in
          let _, pos, elim = find_helper_arg info.term_info (EConstr.to_constr (project gl) f) fargs in
          let id = pf_get_new_id id gl in
-         let occs = Locusops.allHyps in
+         let hyps = Id.Set.elements (hyps_after (project gl) (pos - snd chop) before) in
+         let occs = Some (List.map (fun h -> (Locus.AllOccurrences, h), Locus.InHyp) hyps) in
+         let occs = Locus.{ onhyps = occs; concl_occs = NoOccurrences } in
          let newconcl =
            let fnapp = change_in_app f fargs pos (mkVar id) in
            let indapp = change_in_app ind before (pos - snd chop) (mkVar id) in
            mkApp (indapp, [| fnapp |])
          in
          tclTHENLIST
-          [to82 (letin_tac None (Name id) elim None occs);
-           to82 (convert_concl_no_check newconcl DEFAULTcast);
+          [observe "letin" (to82 (letin_pat_tac true None (Name id) (project gl, elim) occs));
+           observe "convert concl" (to82 (convert_concl_no_check newconcl DEFAULTcast));
            Proofview.V82.of_tactic (clear_body [id]);
            aux_ind_fun info chop unfs unfids s] gl
       | _ -> tclFAIL 0 (str"Unexpected refinement goal in functional induction proof") gl