C.Lambda
(ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
in
- let fresh_meta = ProofEngineHelpers.new_meta proof in
- let irl =
- ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+ let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
let (proof',goals) =
C.Lambda
(ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
in
- let fresh_meta = ProofEngineHelpers.new_meta proof in
+ let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let irl =
- ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
let (proof',goals) =
let wty = CicTypeChecker.type_of_aux' metasenv context what in
try
if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
- then T.thens
- ~start:(
- P.cut_tac
- (C.Appl [
- (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; (* quale uguaglianza usare, eq o eqT ? *)
- wty ;
- what ;
- with_what]))
- ~continuations:[
- T.then_
- ~start:(rewrite_simpl_tac ~term:(C.Rel 1))
- ~continuation:(
- ProofEngineStructuralRules.clear
- ~hyp:(List.hd context)) ;
- T.id_tac]
- ~status
+ then
+ let equality =
+ match CicTypeChecker.type_of_aux' metasenv context wty with
+ C.Sort C.Set -> "cic:/Coq/Init/Logic/eq.ind"
+ | C.Sort C.Type
+ | C.Sort C.CProp
+ | C.Sort C.Prop -> "cic:/Coq/Init/Logic_Type/eqT.ind"
+ | _ -> assert false
+ in
+ T.thens
+ ~start:(
+ P.cut_tac
+ (C.Appl [
+ (C.MutInd ((U.uri_of_string equality), 0, [])) ;
+ wty ;
+ what ;
+ with_what]))
+ ~continuations:[
+ T.then_
+ ~start:(rewrite_simpl_tac ~term:(C.Rel 1))
+ ~continuation:(
+ ProofEngineStructuralRules.clear
+ ~hyp:(List.hd context)) ;
+ T.id_tac]
+ ~status
else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
with (Failure "hd") -> raise (ProofEngineTypes.Fail "Replace: empty context")
;;