From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 1 Feb 2009 00:54:40 +0100
Subject: Imported Upstream version 8.2~rc2+dfsg

---
 interp/constrintern.mli | 29 +++++++++++++----------------
 1 file changed, 13 insertions(+), 16 deletions(-)

(limited to 'interp/constrintern.mli')

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index ea7020be..c5371255 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: constrintern.mli 11024 2008-05-30 12:41:39Z msozeau $ i*)
+(*i $Id: constrintern.mli 11739 2009-01-02 19:33:19Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -39,8 +39,10 @@ open Pretyping
    argument associates a list of implicit positions and scopes to
    identifiers declared in the [rel_context] of [env] *)
 
+type var_internalisation_type = Inductive | Recursive | Method 
+    
 type var_internalisation_data =
-    identifier list * Impargs.implicits_list * scope_name option list
+  var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list
 
 type implicits_env = (identifier * var_internalisation_data) list
 type full_implicits_env = identifier list * implicits_env
@@ -65,7 +67,7 @@ val intern_pattern : env -> cases_pattern_expr ->
   Names.identifier list *
     ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
 
-val intern_context : evar_map -> env -> local_binder list -> raw_binder list
+val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list
 
 (*s Composing internalisation with pretyping *)
 
@@ -111,8 +113,9 @@ val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
 
 (* Interprets constr patterns *)
 
-val interp_constrpattern : 
-  evar_map -> env -> constr_expr -> patvar list * constr_pattern
+val intern_constr_pattern : 
+  evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign -> 
+    constr_pattern_expr -> patvar list * constr_pattern
 
 val interp_reference : ltac_sign -> reference -> rawconstr
 
@@ -124,9 +127,10 @@ val interp_binder_evars : evar_defs ref -> env -> name -> constr_expr -> types
 
 (* Interpret contexts: returns extended env and context *)
 
-val interp_context : evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
+val interp_context : ?fail_anonymous:bool -> 
+  evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
 
-val interp_context_evars : 
+val interp_context_evars : ?fail_anonymous:bool -> 
   evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
 
 (* Locating references of constructions, possibly via a syntactic definition *)
@@ -139,15 +143,8 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
 (* Interprets into a abbreviatable constr *)
 
-val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
-  interpretation
+val interp_aconstr : implicits_env -> identifier list * identifier list 
+  -> constr_expr -> interpretation
 
 (* Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
-
-(* Coqdoc utility functions *)
-type coqdoc_state
-val coqdoc_freeze : unit -> coqdoc_state
-val coqdoc_unfreeze : coqdoc_state -> unit
-
-val add_glob : Util.loc -> global_reference -> unit
-- 
cgit v1.2.3