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/cases.mli | |
| 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/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 9016ca5f3..9f26ae9ce 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -8,9 +8,9 @@ open Names open Term -open EConstr open Evd open Environ +open EConstr open Inductiveops open Glob_term open Evarutil @@ -111,11 +111,11 @@ type 'a pattern_matching_problem = typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } -val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment +val compile : 'a pattern_matching_problem -> unsafe_judgment val prepare_predicate : Loc.t -> (Evarutil.type_constraint -> - Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) -> + Environ.env -> Evd.evar_map ref -> 'a -> unsafe_judgment) -> Environ.env -> Evd.evar_map -> (types * tomatch_type) list -> |