Imported Upstream version 8.5~beta1+dfsg

1 files changed, 80 insertions, 72 deletions

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index b8b3d995..792e6f63 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,15 +8,18 @@
 
 open Names
 open Term
-open Sign
+open Context
 open Evd
 open Environ
 open Libnames
+open Globnames
 open Glob_term
 open Pattern
-open Topconstr
-open Termops
+open Constrexpr
+open Notation_term
 open Pretyping
+open Misctypes
+open Decl_kinds
 
 (** Translation from front abstract syntax of term to untyped terms (glob_constr) *)
 
@@ -37,7 +40,7 @@ open Pretyping
    of [env] *)
 
 type var_internalization_type =
-  | Inductive of identifier list (* list of params *)
+  | Inductive of Id.t list (* list of params *)
   | Recursive
   | Method
   | Variable
@@ -46,14 +49,14 @@ type var_internalization_data =
     var_internalization_type *
       (** type of the "free" variable, for coqdoc, e.g. while typing the
 	  constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
-    identifier list *
+    Id.t list *
       (** impargs to automatically add to the variable, e.g. for "JMeq A a B b"
           in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
     Impargs.implicit_status list * (** signature of impargs of the variable *)
-    scope_name option list (** subscopes of the args of the variable *)
+    Notation_term.scope_name option list (** subscopes of the args of the variable *)
 
 (** A map of free variables to their implicit arguments and scopes *)
-type internalization_env = var_internalization_data Idmap.t
+type internalization_env = var_internalization_data Id.Map.t
 
 val empty_internalization_env : internalization_env
 
@@ -61,79 +64,81 @@ val compute_internalization_data : env -> var_internalization_type ->
   types -> Impargs.manual_explicitation list -> var_internalization_data
 
 val compute_internalization_env : env -> var_internalization_type ->
-  identifier list -> types list -> Impargs.manual_explicitation list list ->
+  Id.t list -> types list -> Impargs.manual_explicitation list list ->
   internalization_env
 
-type ltac_sign = identifier list * unbound_ltac_var_map
+type ltac_sign = {
+  ltac_vars : Id.Set.t;
+  (** Variables of Ltac which may be bound to a term *)
+  ltac_bound : Id.Set.t;
+  (** Other variables of Ltac *)
+}
 
-type glob_binder = (name * binding_kind * glob_constr option * glob_constr)
+val empty_ltac_sign : ltac_sign
+
+type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
 
 (** {6 Internalization performs interpretation of global names and notations } *)
 
-val intern_constr : evar_map -> env -> constr_expr -> glob_constr
+val intern_constr : env -> constr_expr -> glob_constr
 
-val intern_type : evar_map -> env -> constr_expr -> glob_constr
+val intern_type : env -> constr_expr -> glob_constr
 
-val intern_gen : bool -> evar_map -> env ->
+val intern_gen : typing_constraint -> env ->
   ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> glob_constr
 
 val intern_pattern : env -> cases_pattern_expr ->
-  Names.identifier list *
-    ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list
-
-val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
+  Id.t list * (Id.t Id.Map.t * cases_pattern) list
 
-(** {6 Composing internalization with pretyping } *)
+val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
 
-(** Main interpretation function *)
-
-val interp_gen : typing_constraint -> evar_map -> env ->
-  ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
-  constr_expr -> constr
+(** {6 Composing internalization with type inference (pretyping) } *)
 
-(** Particular instances *)
+(** Main interpretation functions expecting evars to be all resolved *)
 
-val interp_constr : evar_map -> env ->
-  constr_expr -> constr
+val interp_constr : env -> evar_map -> ?impls:internalization_env ->
+  constr_expr -> constr Evd.in_evar_universe_context
 
-val interp_type : evar_map -> env -> ?impls:internalization_env ->
-  constr_expr -> types
+val interp_casted_constr : env -> evar_map -> ?impls:internalization_env ->
+  constr_expr -> types -> constr Evd.in_evar_universe_context
 
-val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
+val interp_type : env -> evar_map -> ?impls:internalization_env ->
+  constr_expr -> types Evd.in_evar_universe_context
 
-val interp_open_constr_patvar   : evar_map -> env -> constr_expr -> evar_map * constr
+(** Main interpretation function expecting evars to be all resolved *)
 
-val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
-  constr_expr -> types -> constr
+val interp_open_constr   : env -> evar_map -> constr_expr -> evar_map * constr
 
-(** Accepting evars and giving back the manual implicits in addition. *)
+(** Accepting unresolved evars *)
 
-val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env ->
-  ?impls:internalization_env -> constr_expr -> types -> constr * Impargs.manual_implicits
+val interp_constr_evars : env -> evar_map ref ->
+  ?impls:internalization_env -> constr_expr -> constr
 
-val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
-  env -> ?impls:internalization_env ->
-  constr_expr -> types * Impargs.manual_implicits
+val interp_casted_constr_evars : env -> evar_map ref ->
+  ?impls:internalization_env -> constr_expr -> types -> constr
 
-val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
-  env -> ?impls:internalization_env ->
-  constr_expr -> constr * Impargs.manual_implicits
+val interp_type_evars : env -> evar_map ref ->
+  ?impls:internalization_env -> constr_expr -> types
 
-val interp_casted_constr_evars : evar_map ref -> env ->
-  ?impls:internalization_env -> constr_expr -> types -> constr
+(** Accepting unresolved evars and giving back the manual implicit arguments *)
 
-val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env ->
-  constr_expr -> types
+val interp_constr_evars_impls : env -> evar_map ref ->
+  ?impls:internalization_env -> constr_expr ->
+  constr * Impargs.manual_implicits
 
-(** {6 Build a judgment  } *)
+val interp_casted_constr_evars_impls : env -> evar_map ref ->
+  ?impls:internalization_env -> constr_expr -> types ->
+  constr * Impargs.manual_implicits
 
-val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
+val interp_type_evars_impls : env -> evar_map ref ->
+  ?impls:internalization_env -> constr_expr ->
+  types * Impargs.manual_implicits
 
 (** Interprets constr patterns *)
 
 val intern_constr_pattern :
-  evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
+  env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
     constr_pattern_expr -> patvar list * constr_pattern
 
 (** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
@@ -144,39 +149,42 @@ val interp_reference : ltac_sign -> reference -> glob_constr
 
 (** Interpret binders *)
 
-val interp_binder  : evar_map -> env -> name -> constr_expr -> types
+val interp_binder  : env -> evar_map -> Name.t -> constr_expr -> 
+  types Evd.in_evar_universe_context
 
-val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types
+val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
 
 (** Interpret contexts: returns extended env and context *)
 
-val interp_context_gen : (env -> glob_constr -> types) ->
-  (env -> glob_constr -> unsafe_judgment) ->
+val interp_context_evars :
   ?global_level:bool -> ?impl_env:internalization_env ->
-  evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
-  
-val interp_context : ?global_level:bool -> ?impl_env:internalization_env ->
-  evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+  env -> evar_map ref -> local_binder list ->
+  internalization_env * ((env * rel_context) * Impargs.manual_implicits)
 
-val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env ->
-  evar_map ref -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+(* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
+(*   (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
+(*   ?global_level:bool -> ?impl_env:internalization_env -> *)
+(*   env -> evar_map -> local_binder list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
+  
+(* val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> *)
+(*   env -> evar_map -> local_binder list ->  *)
+(*   internalization_env *  *)
+(*   ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
 
 (** Locating references of constructions, possibly via a syntactic definition 
    (these functions do not modify the glob file) *)
 
-val is_global : identifier -> bool
-val construct_reference : named_context -> identifier -> constr
-val global_reference : identifier -> constr
-val global_reference_in_absolute_module : dir_path -> identifier -> constr
-
-(** Interprets a term as the left-hand side of a notation; the boolean
-    list is a set and this set is [true] for a variable occurring in
-    term position, [false] for a variable occurring in binding
-    position; [true;false] if in both kinds of position *)
-val interp_aconstr : ?impls:internalization_env ->
-  (identifier * notation_var_internalization_type) list ->
-  (identifier * identifier) list -> constr_expr ->
-  (identifier * (subscopes * notation_var_internalization_type)) list * aconstr
+val is_global : Id.t -> bool
+val construct_reference : named_context -> Id.t -> constr
+val global_reference : Id.t -> constr
+val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
+
+(** Interprets a term as the left-hand side of a notation. The returned map is
+    guaranteed to have the same domain as the input one. *)
+val interp_notation_constr : ?impls:internalization_env ->
+  notation_interp_env -> constr_expr ->
+  (subscopes * notation_var_internalization_type) Id.Map.t *
+  notation_constr
 
 (** Globalization options *)
 val parsing_explicit : bool ref