From c75bfdd4162050012614b70a68eff57fc3eabcc4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 31 Oct 2002 15:13:58 +0000 Subject: [PATCH] Several bug-fixes: - URIs shortened - Assumption did not lift the hypothesis ==> the unification always failed --- helm/gTopLevel/variousTactics.ml | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml index d2f168ce9..53a1347ad 100644 --- a/helm/gTopLevel/variousTactics.ml +++ b/helm/gTopLevel/variousTactics.ml @@ -70,13 +70,13 @@ let symmetry_tac ~status:(proof, goal) = let (_,metasenv,_,_) = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in match (R.whd context ty) with - (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind")) -> + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> PrimitiveTactics.apply_tac ~status:(proof,goal) - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/sym_eq.con", [])) + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con", [])) | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> PrimitiveTactics.apply_tac ~status:(proof,goal) - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con", [])) + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con", [])) | _ -> raise (ProofEngineTypes.Fail "Symmetry failed") ;; @@ -90,18 +90,20 @@ let transitivity_tac ~term ~status:((proof, goal) as status) = let (_,metasenv,_,_) = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in match (R.whd context ty) with - (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind")) -> + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> Tl.thens ~start:(PrimitiveTactics.apply_tac - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/trans_eq.con", []))) - ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac] + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", []))) + ~continuations: + [Tl.id_tac ; Tl.id_tac ; PrimitiveTactics.exact_tac ~term] ~status | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> Tl.thens ~start:(PrimitiveTactics.apply_tac - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/trans_eqT.con", []))) - ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac] + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", []))) + ~continuations: + [Tl.id_tac ; Tl.id_tac ; PrimitiveTactics.exact_tac ~term] ~status | _ -> raise (ProofEngineTypes.Fail "Transitivity failed") @@ -114,6 +116,7 @@ let assumption_tac ~status:((proof,goal) as status) = let module C = Cic in let module R = CicReduction in let module T = CicTypeChecker in + let module S = CicSubstitution in let _,metasenv,_,_ = proof in let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let rec find n = function @@ -124,8 +127,11 @@ let assumption_tac ~status:((proof,goal) as status) = | None -> prerr_endline("#### None") ); *) (match hd with - (Some (_, C.Decl t)) when (R.are_convertible context t ty) -> n - | (Some (_, C.Def t)) when (R.are_convertible context (T.type_of_aux' metasenv context t) ty) -> n + (Some (_, C.Decl t)) when + (R.are_convertible context (S.lift n t) ty) -> n + | (Some (_, C.Def t)) when + (R.are_convertible context + (T.type_of_aux' metasenv context (S.lift n t)) ty) -> n | _ -> find (n+1) tl ) | [] -> raise (ProofEngineTypes.Fail "No such assumption") -- 2.39.2