From 77f8b2363ac3e90587b93806e5780f4fff96ecc7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 3 May 2000 18:03:22 +0000
Subject: Ajout get_reference

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@404 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/hipattern.ml  | 8 ++++++++
 tactics/hipattern.mli | 5 +++++
 2 files changed, 13 insertions(+)

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index ccc073b1a5..703bfb7786 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -55,6 +55,14 @@ let (squeleton_stock : (int list * constr) Stock.stock) =
 let put_squel = Stock.stock squeleton_stock
 let get_squel_core = Stock.retrieve squeleton_stock
 
+(* Sera mieux avec des noms qualifiés *)
+let get_reference mods s =
+  if list_subset mods (Library.loaded_modules()) then
+    try Declare.global_reference CCI (id_of_string s)
+    with Not_found ->
+      error ("get_reference: "^s^"is not defined in the given modules")
+  else error "The required modules are not open"
+
 (*
 let dest_somatch n pat =
   let _,m = get_pat pat in
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index ddba560af5..3ec63908fe 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -69,6 +69,11 @@ val put_squel          : module_mark -> string -> marked_term
 val raw_sopattern_of_compattern : Environ.env -> Coqast.t -> constr
 i*)
 
+(* [get_reference mods id] interprets [id] as a global identifier
+   assuming defined in the modules listed in [mods] *)
+
+val get_reference : string list -> string -> constr
+
 (*s Second part : Given a term with second-order variables in it,
    represented by Meta's, and possibly applied using \verb!XTRA[$SOAPP]! to
    terms, this function will perform second-order, binding-preserving,
-- 
cgit v1.2.3