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 /pretyping/classops.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 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index ad43bf322..9011186a3 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -319,7 +319,7 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; let subst, ctx = Universes.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c and t' = Vars.subst_univs_level_constr subst t in - (make_judge c' t', b, b'), ctx + (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx (* pretty-print functions are now in Pretty *) (* rajouter une coercion dans le graphe *) |