diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-11 21:55:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:47 +0100 |
| commit | 0489e8b56d7e10f7111c0171960e25d32201b963 (patch) | |
| tree | d0d71a6a239a7297faea5707bdc88edba6a98e83 /pretyping/typing.ml | |
| parent | cbea91d815f134d63d02d8fb1bd78ed97db28cd1 (diff) | |
Clenv API using EConstr.
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index cf58a0b66..29697260f 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -40,6 +40,7 @@ let meta_type evd mv = let ty = try Evd.meta_ftype evd mv with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in + let ty = Evd.map_fl EConstr.of_constr ty in meta_instance evd ty let constant_type_knowing_parameters env sigma cst jl = @@ -256,7 +257,7 @@ let rec execute env evdref cstr = let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in match EConstr.kind !evdref cstr with | Meta n -> - { uj_val = cstr; uj_type = EConstr.of_constr (meta_type !evdref n) } + { uj_val = cstr; uj_type = meta_type !evdref n } | Evar ev -> let ty = EConstr.existential_type !evdref ev in |