From 1db568d3dc88d538f975377bb4d8d3eecd87872c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Aug 2017 19:05:57 +0200
Subject: 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.
---
 vernac/command.ml       | 2 +-
 vernac/vernacentries.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index 0d6fd24cd1..32ab5401a0 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -367,7 +367,7 @@ let prepare_param = function
     
 let rec check_anonymous_type ind =
   let open Glob_term in
-    match ind.CAst.v with
+    match DAst.get ind with
     | GSort (GType []) -> true
     | GProd ( _, _, _, e) 
     | GLetIn (_, _, _, e)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 8738e58e82..d2ba9eb1cc 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1230,7 +1230,7 @@ let vernac_reserve bl =
     let env = Global.env() in
     let sigma = Evd.from_env env in
     let t,ctx = Constrintern.interp_type env sigma c in
-    let t = Detyping.detype false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in
+    let t = Detyping.detype Detyping.Now false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in
     let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl
-- 
cgit v1.2.3