New: refinement is now used to disambiguate parsing.

[helm.git] / helm / gTopLevel / primitiveTactics.ml

diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml
index 21d5d67c6fd8bcd4088a26571c64ee771ec2f757..ccd8ccfe0ad63eddcd5c572092a78fd11d2ece72 100644 (file)
--- a/helm/gTopLevel/primitiveTactics.ml
+++ b/helm/gTopLevel/primitiveTactics.ml
@@ -37,18 +37,13 @@ exception WrongUriToVariable of string
 (* and [bo] = Lambda/LetIn [context].(Meta [newmeta])       *)
 (* So, lambda_abstract is the core of the implementation of *)
 (* the Intros tactic.                                       *)
-let lambda_abstract context newmeta ty name =
+let lambda_abstract context newmeta ty mknames =
  let module C = Cic in
   let rec collect_context context =
    function
       C.Cast (te,_)   -> collect_context context te
     | C.Prod (n,s,t)  ->
-       let n' =
-        match n with
-           C.Name _ -> n
-(*CSC: generatore di nomi? Chiedere il nome? *)
-         | C.Anonymous -> C.Name name
-       in
+       let n' = C.Name (mknames n) in
         let (context',ty,bo) =
          collect_context ((Some (n',(C.Decl s)))::context) t
         in
@@ -258,7 +253,7 @@ let apply_tac ~term ~status:(proof, goal) =
           C.MutConstruct (uri,tyno,consno,exp_named_subst')
      | _ -> [],newmeta,[],term
    in
-   let metasenv' = newmetasenvfragment@metasenv in
+   let metasenv' = metasenv@newmetasenvfragment in
 prerr_endline ("^^^^^TERM': " ^ CicPp.ppterm term') ; 
    let termty =
     CicSubstitution.subst_vars exp_named_subst_diff
@@ -269,7 +264,7 @@ prerr_endline ("^^^^^TERMTY: " ^ CicPp.ppterm termty) ;
     let (consthead,newmetas,arguments,_) =
      new_metasenv_for_apply newmeta' proof context termty
     in
-     let newmetasenv = newmetas@metasenv' in
+     let newmetasenv = metasenv'@newmetas in
       let subst,newmetasenv' =
        CicUnification.fo_unif newmetasenv context consthead ty
       in
@@ -278,7 +273,7 @@ prerr_endline ("^^^^^TERMTY: " ^ CicPp.ppterm termty) ;
         let old_uninstantiatedmetas,new_uninstantiatedmetas =
          (* subst_in doesn't need the context. Hence the underscore. *)
          let subst_in _ = CicUnification.apply_subst subst in
-          classify_metas newmeta' in_subst_domain subst_in newmetasenv'
+          classify_metas newmeta in_subst_domain subst_in newmetasenv'
         in
          let bo' =
           apply_subst
@@ -306,13 +301,15 @@ let apply_tac ~term ~status =
   with CicUnification.UnificationFailed as e ->
     raise (Fail (Printexc.to_string e))
 
-let intros_tac ~name ~status:(proof, goal) =
+let intros_tac ~status:(proof, goal) =
  let module C = Cic in
  let module R = CicReduction in
   let (_,metasenv,_,_) = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
    let newmeta = new_meta ~proof in
-    let (context',ty',bo') = lambda_abstract context newmeta ty name in
+    let (context',ty',bo') =
+     lambda_abstract context newmeta ty (ProofEngineHelpers.fresh_name)
+    in
      let (newproof, _) =
        subst_meta_in_proof proof metano bo' [newmeta,context',ty']
      in
@@ -503,14 +500,16 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*)
                       List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
 ;;
 
-let elim_simpl_intros_tac ~term =
+(* The simplification is performed only on the conclusion *)
+let elim_intros_simpl_tac ~term =
  Tacticals.then_ ~start:(elim_tac ~term)
   ~continuation:
-   (Tacticals.then_ ~start:ReductionTactics.simpl_tac
-     ~continuation:(intros_tac ~name:"FOO"))
+   (Tacticals.thens
+     ~start:intros_tac
+     ~continuations:
+       [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None])
 ;;
 
-
 exception NotConvertible
 
 (*CSC: Bug (or feature?). [with_what] is parsed in the context of the goal,  *)