From d0593639fe811c06577b39dc62fb5c2734246fc8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 24 Feb 2004 15:07:38 +0000 Subject: [PATCH] Porting URIs to V8.0. --- helm/ocaml/cic/helmLibraryObjects.ml | 9 --------- helm/ocaml/cic_disambiguation/arit_notation.ml | 13 ------------- helm/ocaml/cic_disambiguation/logic_notation.ml | 2 +- helm/ocaml/tactics/discriminationTactics.ml | 8 +++----- helm/ocaml/tactics/ring.ml | 8 ++++---- 5 files changed, 8 insertions(+), 32 deletions(-) diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml index 83f2d3647..3ff0163d2 100644 --- a/helm/ocaml/cic/helmLibraryObjects.ml +++ b/helm/ocaml/cic/helmLibraryObjects.ml @@ -80,15 +80,6 @@ module Logic = let absurd_URI = uri "cic:/Coq/Init/Logic/absurd.con" end -module Logic_Type = - struct - let eqt_URI = uri "cic:/Coq/Init/Logic_Type/eqT.ind" - let sym_eqt_URI = uri "cic:/Coq/Init/Logic_Type/sym_eqT.con" - - let refl_eqt = mutconstruct eqt_URI 0 1 - let sym_eqt = const sym_eqt_URI - end - module Datatypes = struct let bool_URI = uri "cic:/Coq/Init/Datatypes/bool.ind" diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml index 51faaa6ac..324501eb3 100644 --- a/helm/ocaml/cic_disambiguation/arit_notation.ml +++ b/helm/ocaml/cic_disambiguation/arit_notation.ml @@ -120,16 +120,3 @@ let _ = Cic.Appl [ Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); Cic.Implicit (Some `Type); t1; t2 ] ])); - DisambiguateChoices.add_symbol_choice "neq" - ("not equal to (sort Type)", - (fun env _ args -> - let t1, t2 = - match args with - | [t1; t2] -> t1, t2 - | _ -> raise DisambiguateChoices.Invalid_choice - in - Cic.Appl [ const HelmLibraryObjects.Logic.not_URI; - Cic.Appl [ - Cic.MutInd (HelmLibraryObjects.Logic_Type.eqt_URI, 0, []); - Cic.Implicit (Some `Type); t1; t2 ] ])); - diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml index 885cc2140..f622ce034 100644 --- a/helm/ocaml/cic_disambiguation/logic_notation.ml +++ b/helm/ocaml/cic_disambiguation/logic_notation.ml @@ -74,7 +74,7 @@ let _ = | _ -> raise DisambiguateChoices.Invalid_choice in Cic.Appl [ - Cic.MutInd (HelmLibraryObjects.Logic_Type.eqt_URI, 0, []); + Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); Cic.Implicit (Some `Type); t1; t2 ])); DisambiguateChoices.add_binary_op "and" "logical and" diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 15d7968d3..5523c137c 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -35,8 +35,7 @@ let rec injection_tac ~term ~status:((proof, goal) as status) = let termty = (CicTypeChecker.type_of_aux' metasenv context term) in (match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) - or (U.eq equri Logic_Type.eqt_URI) -> ( + when (U.eq equri Logic.eq_URI) -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> ( @@ -87,8 +86,7 @@ and injection1_tac ~term ~i ~status:((proof, goal) as status) = let termty = (CicTypeChecker.type_of_aux' metasenv context term) in match termty with (* an equality *) (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) or - (U.eq equri Logic_Type.eqt_URI) -> ( + when (U.eq equri Logic.eq_URI) -> ( match tty with (* some inductive type *) (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> @@ -211,7 +209,7 @@ let discriminate'_tac ~term ~status:((proof, goal) as status) = let termty = (CicTypeChecker.type_of_aux' metasenv context term) in match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) or (U.eq equri Logic_Type.eqt_URI) -> ( + when (U.eq equri Logic.eq_URI) -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index bd9c15136..fb5caa302 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -190,7 +190,7 @@ exception GoalUnringable *) let ringable = let is_equality = function - | Cic.MutInd (uri, 0, []) when (eq uri Logic_Type.eqt_URI) -> true + | Cic.MutInd (uri, 0, []) when (eq uri Logic.eq_URI) -> true | _ -> false in let is_real = function @@ -447,7 +447,7 @@ let purge_hyps_tac ~count ~status:(proof, goal as status) = *) let ring_tac ~status:((proof, goal) as status) = warn "in Ring tactic"; - let eqt = mkMutInd (Logic_Type.eqt_URI, 0) [] in + let eqt = mkMutInd (Logic.eq_URI, 0) [] in let r = Reals.r in let metasenv = metasenv_of_status ~status in let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in @@ -473,7 +473,7 @@ let ring_tac ~status:((proof, goal) as status) = "exact sym_eqt su t1 ...", exact_tac ~term:( Cic.Appl - [mkConst Logic_Type.sym_eqt_URI + [mkConst Logic.sym_eq_URI [equality_is_a_congruence_A, Reals.r; equality_is_a_congruence_x, t1'' ; equality_is_a_congruence_y, t1 @@ -511,7 +511,7 @@ let ring_tac ~status:((proof, goal) as status) = exact_tac ~term:( Cic.Appl - [mkConst Logic_Type.sym_eqt_URI + [mkConst Logic.sym_eq_URI [equality_is_a_congruence_A, Reals.r; equality_is_a_congruence_x, t2'' ; equality_is_a_congruence_y, t2 -- 2.39.2