added a (for the moment) dummy field _subst to ProofengineTypes.proof.

[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 64db996667879cd10efb1adf0ad83b7032fd2a94..aeb0c0751286285b637a1cff94aae6854ee3cae4 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -52,9 +52,13 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name =
       match ty with 
         C.Cast (te,_)   -> collect_context context howmany do_whd te 
       | C.Prod (n,s,t)  ->
-         let n' = mk_fresh_name metasenv context n ~typ:s in
+        let n' = mk_fresh_name metasenv context n ~typ:s in
           let (context',ty,bo) =
-           let ctx = (Some (n',(C.Decl s)))::context in
+           let entry = match n' with
+             | C.Name _    -> Some (n',(C.Decl s))
+             | C.Anonymous -> None
+          in
+          let ctx = entry :: context in
            collect_context ctx (howmany - 1) do_whd t 
           in
            (context',ty,C.Lambda(n',s,bo))
@@ -257,7 +261,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
-  let (_,metasenv,_,_, _) = proof in
+  let (_,metasenv,_subst,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
@@ -321,7 +325,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
    let subst_in =
      (* if we just apply the subtitution, the type is irrelevant:
               we may use Implicit, since it will be dropped *)
-     CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
+      ((metano,(context,bo',Cic.Implicit None))::subst)
    in
    let (newproof, newmetasenv''') = 
     ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
@@ -365,13 +369,11 @@ let apply_tac ~term =
   PET.mk_tactic (apply_tac ~term)
 
 let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()=
- let intros_tac
-  ?(mk_fresh_name_callback = (FreshNamesGenerator.mk_fresh_name ~subst:[])) ()
-  (proof, goal)
+ let intros_tac (proof, goal)
  =
   let module C = Cic in
   let module R = CicReduction in
-   let (_,metasenv,_,_, _) = proof in
+   let (_,metasenv,_subst,_,_, _) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
      let (context',ty',bo') =
@@ -383,7 +385,7 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_
       in
        (newproof, [newmeta])
  in
-  PET.mk_tactic (intros_tac ~mk_fresh_name_callback ())
+  PET.mk_tactic intros_tac
   
 let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
  let cut_tac
@@ -391,7 +393,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:
   term (proof, goal)
  =
   let module C = Cic in
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in
     let newmeta2 = newmeta1 + 1 in
@@ -426,7 +428,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
   term (proof, goal)
  =
   let module C = Cic in
-   let curi,metasenv,pbo,pty, attrs = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
    (* occur check *)
    let occur i t =
      let m = CicUtil.metas_of_term t in 
@@ -462,7 +464,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
 let exact_tac ~term =
  let exact_tac ~term (proof, goal) =
   (* Assumption: the term bo must be closed in the current context *)
-  let (_,metasenv,_,_, _) = proof in
+  let (_,metasenv,_subst,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let module T = CicTypeChecker in
   let module R = CicReduction in
@@ -495,7 +497,7 @@ module RT  = ReductionTactics
 let beta_after_elim_tac upto predicate =
    let beta_after_elim_tac status =
       let proof, goal = status in
-      let _, metasenv, _, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, _, ty = CicUtil.lookup_meta goal metasenv in
       let mk_pattern ~equality ~upto ~predicate ty =
          (* code adapted from ProceduralConversion.generalize *)
@@ -562,7 +564,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
       | _                    -> raise (PET.Fail (lazy "not implemented"))
    in    
    let ugraph = CicUniv.empty_ugraph in
-   let curi, metasenv, proofbo, proofty, attrs = proof in
+   let curi, metasenv, _subst, proofbo, proofty, attrs = proof in
    let conjecture = CicUtil.lookup_meta goal metasenv in
    let metano, context, ty = conjecture in 
     let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in
@@ -684,13 +686,13 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
          ProofEngineHelpers.compare_metasenvs
             ~oldmetasenv:metasenv ~newmetasenv:metasenv''
       in
-      let proof' = curi,metasenv'',proofbo,proofty, attrs in
+      let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
       let proof'', new_goals' =
          PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
       in
       (* The apply_tactic can have closed some of the new_goals *)
       let patched_new_goals =
-         let (_,metasenv''',_,_, _) = proof'' in
+         let (_,metasenv''',_subst,_,_, _) = proof'' in
          List.filter
             (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
            new_goals @ new_goals'
@@ -706,13 +708,13 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
    PET.mk_tactic elim_tac
 ;;
 
-let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
+let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
  let cases_tac ~term (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,proofbo,proofty, attrs) = proof in
+  let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
   let termty = CicReduction.whd context termty in
@@ -823,13 +825,13 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
     ProofEngineHelpers.compare_metasenvs
       ~oldmetasenv:metasenv ~newmetasenv:metasenv''
   in
-  let proof' = curi,metasenv'',proofbo,proofty, attrs in
+  let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
   let proof'', new_goals' =
     PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
   in
   (* The apply_tactic can have closed some of the new_goals *)
   let patched_new_goals =
-    let (_,metasenv''',_,_,_) = proof'' in
+    let (_,metasenv''',_subst,_,_,_) = proof'' in
       List.filter
         (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
         new_goals @ new_goals'
@@ -864,7 +866,7 @@ let letout_tac =
    let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
    let term = C.Sort C.Set in
    let letout_tac (proof, goal) =
-      let curi, metasenv, pbo, pty, attrs = proof in
+      let curi, metasenv, _subst, pbo, pty, attrs = proof in
       let metano, context, ty = CicUtil.lookup_meta goal metasenv in
       let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
       let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in