diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-11 00:29:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:27 +0100 |
| commit | ca993b9e7765ac58f70740818758457c9367b0da (patch) | |
| tree | a813ef9a194638afbb09cefe1d1e2bce113a9d84 /proofs/clenv.ml | |
| parent | c2855a3387be134d1220f301574b743572a94239 (diff) | |
Making judgment type generic over the type of inner constrs.
This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.
Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
Diffstat (limited to 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 2d621e97c..956be88c8 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -669,12 +669,14 @@ let evar_of_binder holes = function user_err (str "No such binder.") let define_with_type sigma env ev c = + let c = EConstr.of_constr c in let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in - let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in + let ty = Retyping.get_type_of env sigma c in + let ty = EConstr.of_constr ty in let j = Environ.make_judge c ty in let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j (EConstr.of_constr t) in let (ev, _) = destEvar ev in - let sigma = Evd.define ev j.Environ.uj_val sigma in + let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in sigma let solve_evar_clause env sigma hyp_only clause = function |