From 67b8fba4209c407c94ed8d54ec78352397d82f59 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 4 Sep 2014 10:37:01 +0200 Subject: 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. --- pretyping/typing.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/typing.mli') 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 -- cgit v1.2.3