From f90fde30288f67b167b68bfd32363eaa20644c5f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Apr 2009 13:43:41 +0000
Subject: - Cleaning (unification of ML names, removal of obsolete code,  
 reorganization of code) and documentation (in pcoq.mli) of the code   for
 parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic   Notation,
 Notation); merged the two copies of interp_entry_name to   avoid they
 diverge. - Added support in Tactic Notation for ne_..._list_sep in general
 and   for (ne_)ident_list(_sep) in particular.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/topconstr.ml  | 7 +++++++
 interp/topconstr.mli | 1 +
 2 files changed, 8 insertions(+)

(limited to 'interp')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 666f9022bd..32595cdc65 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -890,6 +890,12 @@ let rec prod_constr_expr c = function
       List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
       (prod_constr_expr c bl)
 
+let coerce_reference_to_id = function
+  | Ident (_,id) -> id
+  | Qualid (loc,_) ->
+      user_err_loc (loc, "coerce_reference_to_id",
+        str "This expression should be a simple identifier.")
+
 let coerce_to_id = function
   | CRef (Ident (loc,id)) -> (loc,id)
   | a -> user_err_loc
@@ -903,6 +909,7 @@ let coerce_to_name = function
         (constr_loc a,"coerce_to_name",
          str "This expression should be a name.")
 
+
 (* Used in correctness and interface *)
 
 let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1982a08fd3..0b6cf46c59 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -200,6 +200,7 @@ val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> c
 val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
 val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
 
+val coerce_reference_to_id : reference -> identifier
 val coerce_to_id : constr_expr -> identifier located
 val coerce_to_name : constr_expr -> name located
 
-- 
cgit v1.2.3