Cleaning and documenting Clenv.make_evar_clause

1 files changed, 33 insertions, 8 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 5868f1e9b..a302e6448 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -110,14 +110,38 @@ val clenv_push_prod : clausenv -> clausenv
 (** {6 Pretty-print (debug only) } *)
 val pr_clenv : clausenv -> Pp.std_ppcmds
 
-(** {6 Evar version} *)
+(** {6 Evar-based clauses} *)
+
+(** The following code is an adaptation of the [make_clenv_*] functions above,
+    except that it uses evars instead of metas, and naturally fits in the new
+    refinement monad. It should eventually replace all uses of the
+    aforementioned functions.
+
+    A clause is constructed as follows: assume a type [t := forall (x1 : A1) ...
+    (xn : An), T], we instantiate all the [xi] with a fresh evar [ei] and
+    return [T(xi := ei)] together with the [ei] enriched with a bit of
+    additional data. This is the simple part done by [make_evar_clause].
+
+    The problem lies in the fact we want to solve such holes with some
+    [constr bindings]. This entails some subtleties, because the provided terms
+    may only be well-typed up to a coercion, which we can only infer if we have
+    enough typing information. The meta machinery could insert coercions through
+    tricky instantiation delays. The only solution we have now is to delay the
+    tentative resolution of clauses by providing the [solve_evar_clause]
+    function, to be called at a smart enough time.
+*)
 
 type hole = {
   hole_evar : constr;
+  (** The hole itself. Guaranteed to be an evar. *)
   hole_type : types;
+  (** Type of the hole in the current environment. *)
   hole_deps  : bool;
-  (** Dependent in hypotheses then in conclusion *)
+  (** Whether the remainder of the clause was dependent in the hole. Note that
+      because let binders are substituted, it does not mean that it actually
+      appears somewhere in the returned clause. *)
   hole_name : Name.t;
+  (** Name of the hole coming from its binder. *)
 }
 
 type clause = {
@@ -125,13 +149,13 @@ type clause = {
   cl_concl : types;
 }
 
-val make_evar_clause : env -> evar_map -> int option -> types ->
+val make_evar_clause : env -> evar_map -> ?len:int -> types ->
   (evar_map * clause)
 (** An evar version of {!make_clenv_binding}. Given a type [t],
-    [evar_environments env sigma n t bl] tries to eliminate at most [n] products
-    of the type [t] by filling it with evars. It returns the resulting type
-    together with the list of holes generated. Assumes that [t] is well-typed
-    in the environment. *)
+    [evar_environments env sigma ~len t bl] tries to eliminate at most [len]
+    products of the type [t] by filling it with evars. It returns the resulting
+    type together with the list of holes generated. Assumes that [t] is
+    well-typed in the environment. *)
 
 val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings ->
   evar_map
@@ -139,4 +163,5 @@ val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings ->
     in [cl] according to the [bl] argument. Assumes that [bl] are well-typed in
     the environment. The boolean [hyps] is a compatibility flag that allows to
     consider arguments to be dependent only when they appear in hypotheses and
-    not in the conclusion. *)
+    not in the conclusion. This boolean is only used when [bl] is of the form
+    [ImplicitBindings _]. *)