1. bug fixed in generalize_pattern: a lazy const_tac should have been

[helm.git] / helm / software / components / tactics / primitiveTactics.ml

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 7b58517f6883af1927618721852bbd387a0ef75b..db8fe4376686468c076b1ab41995a9c0e5ff5af2 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -743,7 +743,7 @@ let generalize_pattern_tac pattern =
     List.map
      (fun id ->
        let rel,_ = ProofEngineHelpers.find_hyp id context in
-        id,(Some (PET.const_lazy_term rel), [], Some (ProofEngineTypes.hole))
+        id,(Some (fun ctx m u -> CicSubstitution.lift (List.length ctx - List.length context) rel,m,u), [], Some (ProofEngineTypes.hole))
      ) generalize_hyps in
    let tactics =
     List.map
@@ -886,14 +886,27 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
     PET.mk_tactic reorder_pattern
 ;;
 
-let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
- let cases_tac ~term (proof, goal) =
+let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ?(pattern = PET.conclusion_pattern None) term =
+ let cases_tac pattern (proof, goal) =
   let module TC = CicTypeChecker in
   let module U = UriManager in
   let module R = CicReduction in
   let module C = Cic in
   let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+  let pattern = pattern_after_generalize_pattern_tac pattern in
+  let _cpattern =
+   match pattern with 
+     | None, [], Some cpattern ->
+        let rec is_hole =
+         function
+            Cic.Implicit (Some `Hole) -> true
+          | Cic.Prod (Cic.Anonymous,so,tgt) -> is_hole so && is_hole tgt
+          | _ -> false
+        in
+         if not (is_hole cpattern) then
+          raise (PET.Fail (lazy "not implemented"))
+     | _ -> raise (PET.Fail (lazy "not implemented")) in    
   let termty,_ = TC.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
   let termty = CicReduction.whd context termty in
   let (termty,metasenv',arguments,fresh_meta) =
@@ -1016,7 +1029,16 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
     in
     proof'', patched_new_goals
   in
-  PET.mk_tactic (cases_tac ~term)
+   let reorder_pattern ((proof, goal) as status) =
+     let _,metasenv,_,_,_,_ = proof in
+     let conjecture = CicUtil.lookup_meta goal metasenv in
+     let _,context,_ = conjecture in
+     let pattern = ProofEngineHelpers.sort_pattern_hyps context pattern in
+      PET.apply_tactic
+       (Tacticals.then_ ~start:(generalize_pattern_tac pattern)
+         ~continuation:(PET.mk_tactic (cases_tac pattern))) status
+   in
+    PET.mk_tactic reorder_pattern
 ;;