Ajout glob_eq{,T}

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1818 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 22 insertions, 4 deletions

diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml
index 3250c8db7..88548def3 100644
--- a/parsing/coqlib.ml
+++ b/parsing/coqlib.ml
@@ -26,6 +26,12 @@ let glob_S = ConstructRef ((nat_path,0),2)
 
 let glob_My_special_variable_nat = ConstRef myvar_path
 
+let eq_path = make_path ["Coq";"Init";"Logic"] (id_of_string "eq") CCI
+let eqT_path = make_path ["Coq";"Init";"Logic_Type"] (id_of_string "eqT") CCI
+
+let glob_eq = IndRef (eq_path,0)
+let glob_eqT = IndRef (eqT_path,0)
+
 let reference dir s =
   let dir = "Coq"::"Init"::[dir] in
   let id = id_of_string s in
diff --git a/parsing/coqlib.mli b/parsing/coqlib.mli
index 99481982d..b4e66f9f2 100644
--- a/parsing/coqlib.mli
+++ b/parsing/coqlib.mli
@@ -13,8 +13,10 @@ open Term
 open Pattern
 (*i*)
 
-(*s This module collects the global references of the standard library
-    used in ocaml files *)
+(*s This module collects the global references, constructions and
+    patterns of the standard library used in ocaml files *)
+
+(*s Global references *)
 
 (* Natural numbers *)
 val glob_nat : global_reference
@@ -24,6 +26,18 @@ val glob_S : global_reference
 (* Special variable for pretty-printing of constant naturals *)
 val glob_My_special_variable_nat : global_reference
 
+(* Equality *)
+val glob_eq : global_reference
+val glob_eqT : global_reference
+
+(*s Constructions and patterns related to Coq initial state are unknown
+   at compile time. Therefore, we can only provide methods to build
+   them at runtime. This is the purpose of the [constr delayed] and
+   [constr_pattern delayed] types. Objects of this time needs to be
+   applied to [()] to get the actual constr or pattern at runtime *)
+
+type 'a delayed = unit -> 'a
+
 (*s For Equality tactics *)
 type coq_sigma_data = {
   proj1 : constr;
@@ -35,8 +49,6 @@ type coq_sigma_data = {
 val build_sigma_set : unit -> coq_sigma_data
 val build_sigma_type : unit -> coq_sigma_data
 
-type 'a delayed = unit -> 'a
-
 type coq_leibniz_eq_data = {
   eq   : constr delayed;
   ind  : constr delayed;