diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 10:37:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 15:43:33 +0200 |
| commit | 67b8fba4209c407c94ed8d54ec78352397d82f59 (patch) | |
| tree | 5c78c966e95f957002f55ebd2e09ea7bebab83d8 /pretyping/typing.mli | |
| parent | 3806d567af6b1feee2c8f196199eee4208a8551d (diff) | |
Proofview refiner is now type-safe by default.
In order not to be too costly, there is an [unsafe] flag to be set if the
tactic does not have to check that the partial proof term is well-typed (to
be used with caution though).
This patch breaks one [fix]-based example in the refine test-suite, but a huge
development like CompCert still goes through.
Diffstat (limited to 'pretyping/typing.mli')
| -rw-r--r-- | pretyping/typing.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 8700df52a..1d651e0c1 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -25,7 +25,7 @@ val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types val sort_of : env -> evar_map ref -> types -> sorts (** Typecheck a term has a given type (assuming the type is OK) *) -val check : env -> evar_map -> constr -> types -> unit +val check : env -> evar_map ref -> constr -> types -> unit (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types |