Apply_with_subst now returns a subst with a correct type for the meta.

[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 5310fea7e09a6638bb7b5181053748ac3fba0160..5c7af528f04df92dd4f3df1e8069a72969d5fbf6 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -234,12 +234,13 @@ let
     new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
 ;;
 
-let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
+let new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty termty goal_arity =
   let (consthead,newmetasenv,arguments,_) =
    TermUtil.saturate_term newmeta' metasenv' context termty
     goal_arity in
   let subst,newmetasenv',_ = 
-   CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
+   CicUnification.fo_unif_subst 
+     subst context newmetasenv consthead ty CicUniv.empty_ugraph
   in
   let t = 
     if List.length arguments = 0 then term' else Cic.Appl (term'::arguments)
@@ -301,7 +302,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
    let subst,newmetasenv',t = 
     let rec add_one_argument n =
      try
-      new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
+      new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty
         termty n
      with CicUnification.UnificationFailure _ when n > 0 ->
       add_one_argument (n - 1)
@@ -326,7 +327,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
     ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
      newmetasenv''
    in
-   let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in
+   let subst = ((metano,(context,bo',ty))::subst) in
    subst,
    (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
    max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)
@@ -700,22 +701,36 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
     let n_right_args = List.length right_args in
     let n_lambdas = n_right_args + 1 in
     let lifted_ty = CicSubstitution.lift n_lambdas ty in
-    let replace = ProofEngineReduction.replace_lifting
-       ~equality:(CicUtil.alpha_equivalence)
-    in
     let captured_ty = 
       let what = 
-        List.map (CicSubstitution.lift n_lambdas) (right_args@[term])
+        List.map (CicSubstitution.lift n_lambdas) (right_args)
       in
-      let with_what = 
+      let with_what meta = 
         let rec mkargs = function 
-          | 0 -> []
-          | 1 -> [Cic.Rel 1]
-          | n -> (Cic.Implicit None)::(mkargs (n-1)) 
+          | 0 -> assert false
+          | 1 -> []
+          | n -> 
+              (if meta then Cic.Implicit None else Cic.Rel n)::(mkargs (n-1)) 
         in
         mkargs n_lambdas 
       in
-      replace ~what ~with_what ~where:lifted_ty
+      let replaced = ref false in
+      let replace = ProofEngineReduction.replace_lifting
+       ~equality:(fun _ a b -> let rc = CicUtil.alpha_equivalence a b in 
+                  if rc then replaced := true; rc)
+       ~context:[]
+      in
+      let captured = 
+        replace ~what:[CicSubstitution.lift n_lambdas term] 
+          ~with_what:[Cic.Rel 1] ~where:lifted_ty
+      in
+      if not !replaced then
+        (* this means the matched term is not there, 
+         * but maybe right params are: we user rels (to right args lambdas) *)
+        replace ~what ~with_what:(with_what false) ~where:captured
+      else
+        (* since the matched is there, rights should be inferrable *)
+        replace ~what ~with_what:(with_what true) ~where:captured
     in
     let captured_term_ty = 
       let term_ty = CicSubstitution.lift n_right_args termty in