From ccb173a440fa2eb7105a692c979253edbfe475ee Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 19 Oct 2016 13:33:28 +0200
Subject: Unification constraint handling (#4763, #5149)

Refine fix for bug #4763, fixing #5149

Tactic [Refine.solve_constraints] and global option

Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of
unification constraints and evar candidates to be solved. run_tactic now calls
[solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics.
The option allows to unset the forced solving unification constraints at
each ".", letting the user control the places where the use of
heuristics is done.

Fix test-suite files too.
---
 engine/proofview.ml  | 4 ----
 engine/proofview.mli | 1 -
 2 files changed, 5 deletions(-)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 855235d2b0..c01879765b 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1157,10 +1157,6 @@ let tclLIFT = Proof.lift
 let tclCHECKINTERRUPT =
    tclLIFT (NonLogical.make Control.check_for_interrupt)
 
-
-
-
-
 (*** Compatibility layer with <= 8.2 tactics ***)
 module V82 = struct
   type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 725445251d..90be2f90ab 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -373,7 +373,6 @@ val mark_as_unsafe : unit tactic
     with given up goals cannot be closed. *)
 val give_up : unit tactic
 
-
 (** {7 Control primitives} *)
 
 (** [tclPROGRESS t] checks the state of the proof after [t]. It it is
-- 
cgit v1.2.3


From 1f36cdefd841526f804bd2dd51c1d88309333376 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Nov 2016 14:47:15 +0100
Subject: Fixes to compile with ocaml 4.01

---
 engine/termops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index 35cacc65b2..697b9a5f15 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -980,7 +980,7 @@ let smash_rel_context sign =
 let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 
 let mem_named_context_val id ctxt =
-  try Environ.lookup_named_val id ctxt; true with Not_found -> false
+  try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false
 
 let compact_named_context_reverse sign =
   let compact l decl =
-- 
cgit v1.2.3