From 9b4927d7fdbbafa7ed372e152e7106b3055dfb99 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 Jul 2010 21:06:06 +0000
Subject: Constrintern: unified push_name_env and push_loc_name_env; made
 location dumping for binders uniformly treated in constrintern.ml (and
 renamed the optional arg of interp_context from fail_anonymous to
 global_level since the flag now also decides whether to dump binders as
 global or local ones); added locations for the variables occurring in the "as
 in" clauses;

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13314 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp/constrintern.mli')

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 326089d37e..1dd221f69b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -155,13 +155,13 @@ val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types
 
 val interp_context_gen : (env -> rawconstr -> types) ->
   (env -> rawconstr -> unsafe_judgment) ->
-  ?fail_anonymous:bool ->
+  ?global_level:bool ->
   evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
   
-val interp_context : ?fail_anonymous:bool ->
+val interp_context : ?global_level:bool ->
   evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
 
-val interp_context_evars : ?fail_anonymous:bool ->
+val interp_context_evars : ?global_level:bool ->
   evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
 
 (** Locating references of constructions, possibly via a syntactic definition 
-- 
cgit v1.2.3