From 0583c44e19ee683efab796bf21904bbfc64fbf1e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 5 Sep 2003 14:31:16 +0000 Subject: [PATCH] Replace is now working also over Type. --- helm/ocaml/tactics/equalityTactics.ml | 40 ++++++++++++++++----------- 1 file changed, 24 insertions(+), 16 deletions(-) diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 1d7c2f69c..1c2a7d37f 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -159,22 +159,30 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) = 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.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") ;; -- 2.39.2