From 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 13 Jun 2018 00:22:57 +0200 Subject: Remove reference name type. reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid. --- plugins/ltac/rewrite.ml | 37 ++++++++++++++++++------------------- 1 file changed, 18 insertions(+), 19 deletions(-) (limited to 'plugins/ltac/rewrite.ml') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index cd04f4ae9a..01c52c413c 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1773,11 +1773,11 @@ let rec strategy_of_ast = function (* By default the strategy for "rewrite_db" is top-down *) -let mkappc s l = CAst.make @@ CAppExpl ((None,CAst.make @@ Libnames.Ident (Id.of_string s),None),l) +let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l) let declare_an_instance n s args = (((CAst.make @@ Name n),None), Explicit, - CAst.make @@ CAppExpl ((None, CAst.make @@ Qualid (qualid_of_string s),None), args)) + CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] @@ -1791,17 +1791,17 @@ let anew_instance global binders instance fields = let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" in anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "reflexivity"),lemma)] + [(qualid_of_ident (Id.of_string "reflexivity"),lemma)] let declare_instance_sym global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric" in anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "symmetry"),lemma)] + [(qualid_of_ident (Id.of_string "symmetry"),lemma)] let declare_instance_trans global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" in anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "transitivity"),lemma)] + [(qualid_of_ident (Id.of_string "transitivity"),lemma)] let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = init_setoid (); @@ -1825,16 +1825,16 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "PreOrder_Reflexive"), lemma1); - (CAst.make @@ Ident (Id.of_string "PreOrder_Transitive"),lemma3)]) + [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); + (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]) | (None, Some lemma2, Some lemma3) -> let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "PER_Symmetric"), lemma2); - (CAst.make @@ Ident (Id.of_string "PER_Transitive"),lemma3)]) + [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); + (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]) | (Some lemma1, Some lemma2, Some lemma3) -> let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in @@ -1842,9 +1842,9 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), lemma1); - (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2); - (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)]) + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]) let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) @@ -1949,16 +1949,15 @@ let add_setoid global binders a aeq t n = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); - (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); - (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) let make_tactic name = let open Tacexpr in - let tacpath = Libnames.qualid_of_string name in - let tacname = CAst.make @@ Qualid tacpath in - TacArg (Loc.tag @@ (TacCall (Loc.tag (tacname, [])))) + let tacqid = Libnames.qualid_of_string name in + TacArg (Loc.tag @@ (TacCall (Loc.tag (tacqid, [])))) let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> @@ -2008,7 +2007,7 @@ let add_morphism glob binders m s n = let instance = (((CAst.make @@ Name instance_id),None), Explicit, CAst.make @@ CAppExpl ( - (None, CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), + (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in -- cgit v1.2.3