Making detyping potentially lazy.

The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.

We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.

Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).

We also fix a regression in the test-suite:

  Mixing laziness and effects is a well-known hell. Here, an exception
  that was raised for mere control purpose was delayed and raised at a
  later time as an anomaly. We make the offending function eager.

1 files changed, 3 insertions, 3 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 5a4c52456..fca7d9851 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -442,11 +442,11 @@ let cc_tactic depth additionnal_terms =
             let open Glob_term in
             let env = Proofview.Goal.env gl in
             let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
-            let hole = CAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in
+            let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in
             let pr_missing (c, missing) =
-              let c = Detyping.detype ~lax:true false [] env sigma c in
+              let c = Detyping.detype Detyping.Now ~lax:true false [] env sigma c in
               let holes = List.init missing (fun _ -> hole) in
-              Printer.pr_glob_constr_env env (CAst.make @@ GApp (c, holes))
+              Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
             in
 	    Feedback.msg_info
 	      (Pp.str "Goal is solvable by congruence but some arguments are missing.");