(* 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
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
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 ~also_in_hypotheses:false ~term:None)
- ~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, *)