diff options
| author | Pierre-Marie Pédrot | 2014-09-04 10:37:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-04 15:43:33 +0200 |
| commit | 67b8fba4209c407c94ed8d54ec78352397d82f59 (patch) | |
| tree | 5c78c966e95f957002f55ebd2e09ea7bebab83d8 /pretyping | |
| 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')
| -rw-r--r-- | pretyping/typing.ml | 5 | ||||
| -rw-r--r-- | pretyping/typing.mli | 2 |
2 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index d2fddabdca..1485b77015 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -263,11 +263,10 @@ and execute_recdef env evdref (names,lar,vdef) = and execute_array env evdref = Array.map (execute env evdref) -let check env evd c t = - let evdref = ref evd in +let check env evdref c t = let j = execute env evdref c in if not (Evarconv.e_cumul env evdref j.uj_type t) then - error_actual_type env j (nf_evar evd t) + error_actual_type env j (nf_evar !evdref t) (* Type of a constr *) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 8700df52a8..1d651e0c1e 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 |