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/refine.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/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index 0ed74c9b3..067764c00 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -133,7 +133,9 @@ let refine ?(unsafe = true) f = (** Useful definitions *) let with_type env evd c t = - let my_type = Retyping.get_type_of env evd (EConstr.of_constr c) in + let c = EConstr.of_constr c in + let my_type = Retyping.get_type_of env evd c in + let my_type = EConstr.of_constr my_type in let j = Environ.make_judge c my_type in let (evd,j') = Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j (EConstr.of_constr t) @@ -147,6 +149,7 @@ let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> let f = { run = fun h -> let Sigma (c, h, p) = f.run h in let sigma, c = with_type env (Sigma.to_evar_map h) c concl in + let c = EConstr.Unsafe.to_constr c in Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) } in refine ?unsafe f |