open ProofEngineHelpers
open ProofEngineTypes
+exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
exception NotAnInductiveTypeToEliminate
-exception NotTheRightEliminatorShape
-exception NoHypothesesFound
exception WrongUriToVariable of string
(* lambda_abstract newmeta ty *)
in
let metasenv' = metasenv@newmetasenvfragment in
let termty,_ =
- CicTypeChecker.type_of_aux' metasenv' context term CicUniv.empty_ugraph in
+ CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph in
let termty =
CicSubstitution.subst_vars exp_named_subst_diff termty
in
-(* prerr_endline ("term:" ^ CicPp.ppterm term);*)
-(* prerr_endline ("termty:" ^ CicPp.ppterm termty);*)
let subst,newmetasenv',t =
try
new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty
in
mk_tactic (intros_tac ~mk_fresh_name_callback ())
-let cut_tac?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
+let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
let cut_tac
?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
term (proof, goal)
in
mk_tactic (cut_tac ~mk_fresh_name_callback term)
-let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
+let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
let letin_tac
?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
term (proof, goal)
| C.Sort C.Set -> "_rec"
| C.Sort C.CProp -> "_rec"
| C.Sort (C.Type _)-> "_rect"
+ | C.Meta (_,_) -> raise TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
| _ -> assert false
in
U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
(Tacticals.thens
~start:(intros_tac ())
~continuations:
- [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None])
+ [ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern])
;;
exception NotConvertible
(*CSC: while [what] can have a richer context (because of binders) *)
(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
(*CSC: Is that evident? Is that right? Or should it be changed? *)
-let change_tac ~what ~with_what =
- let change_tac ~what ~with_what (proof, goal) =
+let change_tac ~what ~with_what ~pattern =
+(*
+ let change_tac ~what ~with_what ~pattern (proof, goal) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
(* are_convertible works only on well-typed terms *)
else
raise (ProofEngineTypes.Fail "Not convertible")
in
- mk_tactic (change_tac ~what ~with_what)
-
+ mk_tactic (change_tac ~what ~with_what ~pattern)
+*) assert false