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.ml  | 5 ++---
 pretyping/typing.mli | 2 +-
 2 files changed, 3 insertions(+), 4 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3