diff options
| -rw-r--r-- | contrib/omega/coq_omega.ml | 3 | ||||
| -rw-r--r-- | contrib/ring/quote.ml | 3 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 3 | ||||
| -rw-r--r-- | tactics/equality.ml | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 3 |
5 files changed, 10 insertions, 5 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 9efa5aa4a..9b3aa0694 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -211,7 +211,8 @@ let recognize_number t = To use the constant Zplus, one must type "Lazy.force coq_Zplus" This is the right way to access to Coq constants in tactics ML code *) -let constant dir s = Declare.global_qualified_reference (make_qualid dir s) +let constant dir s = + Declare.global_absolute_reference (make_path dir (id_of_string s) CCI) (* fast_integer *) let coq_xH = lazy (constant ["fast_integer"] "xH") diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 8ebd8dc61..b3462d8f3 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -112,7 +112,8 @@ open Proof_type We do that lazily, because this code can be linked before the constants are loaded in the environment *) -let constant dir s = Declare.global_qualified_reference (make_qualid dir s) +let constant dir s = + Declare.global_absolute_reference (make_path dir (id_of_string s) CCI) let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm") let coq_Node_vm = lazy (constant ["Quote"] "Node_vm") diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index d2c379659..775724e49 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -25,7 +25,8 @@ open Quote;; let mt_evd = Evd.empty let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com -let constant dir s = Declare.global_qualified_reference (make_qualid dir s) +let constant dir s = + Declare.global_absolute_reference (make_path dir (id_of_string s) CCI) (* Ring_theory *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 96c323d73..83af30949 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -669,7 +669,8 @@ let h_discrHyp = hide_ident_tactic "DiscrHyp" discrHyp let existS_pattern = put_pat mmk "(existS ?1 ?2 ?3 ?4)" let existT_pattern = put_pat mmk "(existT ?1 ?2 ?3 ?4)" -let constant dir s = Declare.global_qualified_reference (make_qualid dir s) +let constant dir s = + Declare.global_absolute_reference (make_path dir (id_of_string s) CCI) let build_sigma_set () = { proj1 = constant ["Specif"] "projS1"; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6d3da97ad..cf9946b8e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1524,7 +1524,8 @@ let contradiction_on_hyp id gl = else error "Not a contradiction" -let constant dir s = Declare.global_qualified_reference (make_qualid dir s) +let constant dir s = + Declare.global_absolute_reference (make_path dir (id_of_string s) CCI) let coq_False = lazy (constant ["Logic"] "False") let coq_not = lazy (constant ["Logic"] "not") |