Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 41 insertions, 35 deletions

diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index b94f9789..47b3ec87 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -1,24 +1,26 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretyping.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** This file implements type inference. It maps [glob_constr]
+   (i.e. untyped terms whose names are located) to [constr]. In
+   particular, it drives complex pattern-matching problems ("match")
+   into elementary ones, insertion of coercions and resolution of
+   implicit arguments. *)
 
-(*i*)
 open Names
 open Sign
 open Term
 open Environ
 open Evd
-open Rawterm
+open Glob_term
 open Evarutil
-(*i*)
 
-(* An auxiliary function for searching for fixpoint guard indexes *)
+(** An auxiliary function for searching for fixpoint guard indexes *)
 
 val search_guard :
     Util.loc -> env -> int list list -> rec_declaration -> int array
@@ -28,30 +30,31 @@ type typing_constraint = OfType of types option | IsType
 type var_map = (identifier * Pattern.constr_under_binders) list
 type unbound_ltac_var_map = (identifier * identifier option) list
 type ltac_var_map = var_map * unbound_ltac_var_map
-type rawconstr_ltac_closure = ltac_var_map * rawconstr
+type glob_constr_ltac_closure = ltac_var_map * glob_constr
+type pure_open_constr = evar_map * constr
 
 module type S =
 sig
 
   module Cases : Cases.S
 
-  (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+  (** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
   val allow_anonymous_refs : bool ref
 
-  (* Generic call to the interpreter from rawconstr to open_constr, leaving
+  (** Generic call to the interpreter from glob_constr to open_constr, leaving
      unresolved holes as evars and returning the typing contexts of
      these evars. Work as [understand_gen] for the rest. *)
 
   val understand_tcc : ?resolve_classes:bool ->
-    evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
+    evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr
 
   val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
-    evar_map ref -> env -> typing_constraint -> rawconstr -> constr
+    evar_map ref -> env -> typing_constraint -> glob_constr -> constr
 
-  (* More general entry point with evars from ltac *)
+  (** More general entry point with evars from ltac *)
 
-  (* Generic call to the interpreter from rawconstr to constr, failing
-     unresolved holes in the rawterm cannot be instantiated.
+  (** Generic call to the interpreter from glob_constr to constr, failing
+     unresolved holes in the glob_constr cannot be instantiated.
 
      In [understand_ltac expand_evars sigma env ltac_env constraint c],
 
@@ -63,56 +66,59 @@ sig
 
   val understand_ltac :
     bool -> evar_map -> env -> ltac_var_map ->
-    typing_constraint -> rawconstr -> evar_map * constr
+    typing_constraint -> glob_constr -> pure_open_constr
 
-  (* Standard call to get a constr from a rawconstr, resolving implicit args *)
+  (** Standard call to get a constr from a glob_constr, resolving implicit args *)
 
   val understand : evar_map -> env -> ?expected_type:Term.types ->
-    rawconstr -> constr
+    glob_constr -> constr
 
-  (* Idem but the rawconstr is intended to be a type *)
+  (** Idem but the glob_constr is intended to be a type *)
 
-  val understand_type : evar_map -> env -> rawconstr -> constr
+  val understand_type : evar_map -> env -> glob_constr -> constr
 
-  (* A generalization of the two previous case *)
+  (** A generalization of the two previous case *)
 
   val understand_gen : typing_constraint -> evar_map -> env ->
-    rawconstr -> constr
+    glob_constr -> constr
 
-  (* Idem but returns the judgment of the understood term *)
+  (** Idem but returns the judgment of the understood term *)
 
-  val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
+  val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment
 
-  (* Idem but do not fail on unresolved evars *)
-  val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment
+  (** Idem but do not fail on unresolved evars *)
+  val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment
 
-  (*i*)
-  (* Internal of Pretyping...
-   *)
+  (**/**)
+  (** Internal of Pretyping... *)
   val pretype :
     type_constraint -> env -> evar_map ref ->
-    ltac_var_map -> rawconstr -> unsafe_judgment
+    ltac_var_map -> glob_constr -> unsafe_judgment
 
   val pretype_type :
     val_constraint -> env -> evar_map ref ->
-    ltac_var_map -> rawconstr -> unsafe_type_judgment
+    ltac_var_map -> glob_constr -> unsafe_type_judgment
 
   val pretype_gen :
     bool -> bool -> bool -> evar_map ref -> env ->
-    ltac_var_map -> typing_constraint -> rawconstr -> constr
+    ltac_var_map -> typing_constraint -> glob_constr -> constr
 
-  (*i*)
+  (**/**)
 
 end
 
 module Pretyping_F (C : Coercion.S) : S
 module Default : S
 
-(* To embed constr in rawconstr *)
+(** To embed constr in glob_constr *)
 
 val constr_in : constr -> Dyn.t
 val constr_out : Dyn.t -> constr
 
-val interp_sort : rawsort -> sorts
-val interp_elimination_sort : rawsort -> sorts_family
+val interp_sort : glob_sort -> sorts
+val interp_elimination_sort : glob_sort -> sorts_family
 
+(** Last chance for solving evars, possibly using external solver *)
+val solve_remaining_evars : bool -> bool ->
+  (env -> evar_map -> existential -> constr) ->
+  env -> evar_map -> pure_open_constr -> pure_open_constr