From 405acea72a67c31ec8554c1f76d51518a5df769a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 28 Sep 2016 15:38:33 +0200
Subject: Remove incorrect assertion in cbn (bug #4822).

This assertion checked that two arguments in the same position were equal,
but in fact, since one might have already been reduced, they are only
convertible (which is too costly to check in an assertion).
---
 pretyping/reductionops.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4ccbc81b47..332d4e0b26 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -166,9 +166,6 @@ module Cst_stack = struct
   let empty = []
   let is_empty = CList.is_empty
 
-  let sanity x y =
-    assert(Term.eq_constr x y)
-
   let drop_useless = function
     | _ :: ((_,_,[])::_ as q) -> q
     | l -> l
@@ -177,9 +174,9 @@ module Cst_stack = struct
     let append2cst = function
       | (c,params,[]) -> (c, h::params, [])
       | (c,params,((i,t)::q)) when i = pred (Array.length t) ->
-	 let () = sanity h t.(i) in (c, params, q)
+	(c, params, q)
       | (c,params,(i,t)::q) ->
-	let () = sanity h t.(i) in (c, params, (succ i,t)::q)
+	(c, params, (succ i,t)::q)
     in
       drop_useless (List.map append2cst cst_l)
 
-- 
cgit v1.2.3


From 875f235dd0413faa34f7d46afc25d2eb90e386e5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Sep 2016 17:01:26 +0200
Subject: Fix bug #4723 and FIXME in API for solve_by_tac

This avoids leakage of universes. Also makes
Program Lemma/Fact work again, it tries to solve the
remaining evars using the obligation tactic.
---
 pretyping/pretyping.ml  | 6 ++++--
 pretyping/pretyping.mli | 4 +++-
 2 files changed, 7 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 46f0219f91..48bf9149d0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -239,10 +239,12 @@ let interp_elimination_sort = function
   | GSet  -> InSet
   | GType _ -> InType
 
+type inference_hook = env -> evar_map -> evar -> evar_map * constr
+
 type inference_flags = {
   use_typeclasses : bool;
   use_unif_heuristics : bool;
-  use_hook : (env -> evar_map -> evar -> constr) option;
+  use_hook : inference_hook option;
   fail_evar : bool;
   expand_evars : bool
 }
@@ -272,7 +274,7 @@ let apply_inference_hook hook evdref pending =
     if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
     then
       try
-        let c = hook sigma evk in
+        let sigma, c = hook sigma evk in
         Evd.define evk c sigma
       with Exit ->
         sigma
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 824bb11aa4..eead48a549 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -47,10 +47,12 @@ val empty_lvar : ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
 
+type inference_hook = env -> evar_map -> evar -> evar_map * constr
+
 type inference_flags = {
   use_typeclasses : bool;
   use_unif_heuristics : bool;
-  use_hook : (env -> evar_map -> evar -> constr) option;
+  use_hook : inference_hook option;
   fail_evar : bool;
   expand_evars : bool
 }
-- 
cgit v1.2.3