diff options
| author | Maxime Dénès | 2017-09-07 12:44:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-07 12:44:47 +0200 |
| commit | 084ef41c98d52078f85831c940d0a073a4ccdb7a (patch) | |
| tree | f1808d72e562f0dd674759f2f447f44cd5da9aad /vernac | |
| parent | 276f08cb053eed175478c4c9359e61fb949742ba (diff) | |
| parent | 1db568d3dc88d538f975377bb4d8d3eecd87872c (diff) | |
Merge PR #914: Making the detyper lazy
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/command.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
2 files changed, 2 insertions, 2 deletions
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 |