From d64b5766aa8de3842edae167ce554c36ff46f947 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Feb 2015 19:48:54 +0100
Subject: Fixing cf6a68b45 on integrating ensure_evar_independent into
 is_constrainable_in.

---
 pretyping/evarsolve.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b01f29a40a..307edcc89a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1017,7 +1017,7 @@ exception CannotProject of evar_map * existential
   of subterms to eventually discard so as to be allowed to keep ti.
 *)
 
-let rec is_constrainable_in top force k (ev,(fv_rels,fv_ids) as g) t =
+let rec is_constrainable_in top force env evd k (ev,(fv_rels,fv_ids) as g) t =
   let f,args = decompose_app_vect t in
   match kind_of_term f with
   | Construct ((ind,_),u) ->
@@ -1025,21 +1025,21 @@ let rec is_constrainable_in top force k (ev,(fv_rels,fv_ids) as g) t =
     if n > Array.length args then true (* We don't try to be more clever *)
     else
       let params = fst (Array.chop n args) in
-      Array.for_all (is_constrainable_in false force k g) params
-  | Ind _ -> Array.for_all (is_constrainable_in false force k g) args
-  | Prod (_,t1,t2) -> is_constrainable_in false force k g t1 && is_constrainable_in false force k g t2
+      Array.for_all (is_constrainable_in false force env evd k g) params
+  | Ind _ -> Array.for_all (is_constrainable_in false force env evd k g) args
+  | Prod (_,t1,t2) -> is_constrainable_in false force env evd k g t1 && is_constrainable_in false force env evd k g t2
   | Evar (ev',_) -> top || not (force || Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
   | Sort _ -> true
-  | _ -> (* We don't try to be more clever *) true
+  | _ -> (* We don't try to be more clever *) not force || noccur_evar env evd ev t
 
-let has_constrainable_free_vars evd aliases force k ev (fv_rels,fv_ids as fvs) t =
+let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids as fvs) t =
   let t = expansion_of_var aliases t in
   match kind_of_term t with
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
-  | _ -> is_constrainable_in true force k (ev,fvs) t
+  | _ -> is_constrainable_in true force env evd k (ev,fvs) t
 
 exception EvarSolvedOnTheFly of evar_map * constr
 
@@ -1049,7 +1049,7 @@ let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (e
   (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
   let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in
   let filter1 = restrict_upon_filter evd evk1
-    (has_constrainable_free_vars evd aliases force k2 evk2 fvs2)
+    (has_constrainable_free_vars env evd aliases force k2 evk2 fvs2)
     argsv1 in
   let candidates1 =
     try restrict_candidates g env evd filter1 ev1 ev2
-- 
cgit v1.2.3


From ebfc19d792492417b129063fb511aa423e9d9e08 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Feb 2015 22:27:53 +0100
Subject: Compensating 6fd763431 on postponing subtyping evar-evar problems.

Pushing pending problems had the side-effect of later solving them in
the opposite order as they arrived, resulting on different complexity
(see e.g. #4076). We now take care of pushing them in reverse order so
that they are treated in the same order.
---
 pretyping/evarsolve.ml | 12 ++++++------
 pretyping/evd.ml       |  4 +++-
 pretyping/evd.mli      |  2 +-
 3 files changed, 10 insertions(+), 8 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 307edcc89a..9f1b118fb3 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -121,11 +121,11 @@ let is_success = function Success _ -> true | UnifFailure _ -> false
 let test_success conv_algo env evd c c' rhs =
   is_success (conv_algo env evd c c' rhs)
 
-let add_conv_oriented_pb (pbty,env,t1,t2) evd =
+let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
   match pbty with
-  | Some true -> add_conv_pb (Reduction.CUMUL,env,t1,t2) evd
-  | Some false -> add_conv_pb (Reduction.CUMUL,env,t2,t1) evd
-  | None -> add_conv_pb (Reduction.CONV,env,t1,t2) evd
+  | Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd
+  | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd
+  | None -> add_conv_pb ~tail (Reduction.CONV,env,t1,t2) evd
 
 (*------------------------------------*
  * Restricting existing evars         *
@@ -1111,13 +1111,13 @@ let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 a
     with CannotProject (evd,ev2) ->
     try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
-    add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
+    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
   else
     try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
     try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
     with CannotProject (evd,ev2) ->
-    add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
+    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
 
 let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let pbty = if force then None else pbty in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 9313e22320..4e38bd4e66 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -779,7 +779,9 @@ let merge_universe_context evd uctx' =
 let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
-let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
+let add_conv_pb ?(tail=false) pb d =
+  if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
+  else {d with conv_pbs = pb::d.conv_pbs}
 
 let evar_source evk d = (find d evk).evar_source
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index cf6ba07c60..48704f75bb 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -397,7 +397,7 @@ type clbinding =
 (** Unification constraints *)
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * constr * constr
-val add_conv_pb :  evar_constraint -> evar_map -> evar_map
+val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map
 
 val extract_changed_conv_pbs : evar_map ->
       (Evar.Set.t -> evar_constraint -> bool) ->
-- 
cgit v1.2.3


From 2734891ab7e90c5b488416d11c3dc41c224773e7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 24 Feb 2015 14:22:02 +0100
Subject: Another bug (de Bruijn) in continuing cf6a68b45 and d64b5766a on
 integrating ensure_evar_independent into is_constrainable_in.

---
 pretyping/evarsolve.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 9f1b118fb3..13c63e9784 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1027,7 +1027,7 @@ let rec is_constrainable_in top force env evd k (ev,(fv_rels,fv_ids) as g) t =
       let params = fst (Array.chop n args) in
       Array.for_all (is_constrainable_in false force env evd k g) params
   | Ind _ -> Array.for_all (is_constrainable_in false force env evd k g) args
-  | Prod (_,t1,t2) -> is_constrainable_in false force env evd k g t1 && is_constrainable_in false force env evd k g t2
+  | Prod (na,t1,t2) -> is_constrainable_in false force env evd k g t1 && is_constrainable_in false force (push_rel (na,None,t1) env) evd k g t2
   | Evar (ev',_) -> top || not (force || Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
-- 
cgit v1.2.3


From f7b29094fe7cc13ea475447bd30d9a8b942f0fef Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 19 Feb 2015 12:08:51 +0100
Subject: [Proofview.tclPROGRESS]: do not consider that trivial goal
 instantiation is progress.

Also compare goals up to evar instantiation (otherwise no progress would be observed when only unification occurs, unless some [nf_evar] is done). Performance look unchanged so far.

Some code from [Evd] which was used only in [tclPROGRESS] have been moved out (and [progress_evar_map] was now dead, so I killed it).

Fixes bugs (one reported directly on coqdev, and #3412).
---
 pretyping/evarutil.ml  |  5 +++++
 pretyping/evarutil.mli |  7 +++++++
 pretyping/evd.ml       | 29 -----------------------------
 pretyping/evd.mli      |  7 -------
 4 files changed, 12 insertions(+), 36 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d286b98e83..0b8cbff36c 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -838,3 +838,8 @@ let subterm_source evk (loc,k) =
     | Evar_kinds.SubEvar (evk) -> evk
     | _ -> evk in
   (loc,Evar_kinds.SubEvar evk)
+
+
+(** Term exploration up to isntantiation. *)
+let kind_of_term_upto sigma t =
+  Constr.kind (Reductionops.whd_evar sigma t)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index f89266a60a..92a3984ba6 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -199,6 +199,13 @@ val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
 exception Uninstantiated_evar of existential_key
 val flush_and_check_evars :  evar_map -> constr -> constr
 
+(** {6 Term manipulation up to instantiation} *)
+
+(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
+    as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the
+    value of [e] in [sigma] is (recursively) used. *)
+val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
+
 (** {6 debug pretty-printer:} *)
 
 val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4e38bd4e66..454c51195b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -568,14 +568,6 @@ type evar_map = {
 
 (*** Lifting primitive from Evar.Map. ***)
 
-(* HH: The progress tactical now uses this function. *)
-let progress_evar_map d1 d2 =
-  let is_new k v =
-    assert (v.evar_body == Evar_empty);
-    EvMap.mem k d2.defn_evars
-  in
-  not (d1 == d2) && EvMap.exists is_new d1.undf_evars
-
 let add_name_newly_undefined naming evk evi (evtoid,idtoev) =
   let id = match naming with
   | Misctypes.IntroAnonymous ->
@@ -1303,27 +1295,6 @@ let e_eq_constr_univs evdref t u =
 let eq_constr_univs_test evd t u =
   snd (eq_constr_univs evd t u)
 
-let eq_named_context_val d ctx1 ctx2 = 
-  ctx1 == ctx2 ||
-    let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
-    let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-      Id.equal i1 i2 && Option.equal (eq_constr_univs_test d) c1 c2 
-      && (eq_constr_univs_test d) t1 t2
-    in List.equal eq_named_declaration c1 c2
-
-let eq_evar_body d b1 b2 = match b1, b2 with
-| Evar_empty, Evar_empty -> true
-| Evar_defined t1, Evar_defined t2 -> eq_constr_univs_test d t1 t2
-| _ -> false
-
-let eq_evar_info d ei1 ei2 =
-  ei1 == ei2 ||
-    eq_constr_univs_test d ei1.evar_concl ei2.evar_concl &&
-    eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) &&
-    eq_evar_body d ei1.evar_body ei2.evar_body
-    (** ppedrot: [eq_constr] may be a bit too permissive here *)
-
-
 (**********************************************************)
 (* Accessing metas *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 48704f75bb..0765b951fd 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -126,10 +126,6 @@ type evar_map
 (** Type of unification state. Essentially a bunch of state-passing data needed
     to handle incremental term construction. *)
 
-val progress_evar_map : evar_map -> evar_map -> bool
-(** Assuming that the second map extends the first one, this says if
-   some existing evar has been refined *)
-
 val empty : evar_map
 (** The empty evar map. *)
 
@@ -204,9 +200,6 @@ val add_constraints : evar_map -> Univ.constraints -> evar_map
 val undefined_map : evar_map -> evar_info Evar.Map.t
 (** Access the undefined evar mapping directly. *)
 
-val eq_evar_info : evar_map -> evar_info -> evar_info -> bool
-(** Compare the evar_info's up to the universe constraints of the evar map. *)
-
 val drop_all_defined : evar_map -> evar_map
 
 (** {6 Instantiating partial terms} *)
-- 
cgit v1.2.3


From 5a7a90e6fc067319e66c8021e696df98883223f0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Feb 2015 08:11:14 +0100
Subject: An optimization on filtering evar instances with let-ins suggested by
 inefficiency #4076.

In an evar context like this one

x:X, y:=f(x), z:Z(x,y) |- ?x : T(x,y,z)

with unification problem

a:A, b:=f(t(a)) |- ?x[x:=t(a);y:=b;z:=u(a,b)] = v(a,b,c)

we now keep y after filtering, iff the name b occurs effectively in
v(a,b,c), while before, we kept it as soon as its expansion f(t(a))
had free variables in v(a,b,c), which was more often, but useless
since the point in keeping a let-in in the instance is precisely to
reuse the name of the let-in while unifying with a right-hand side
which mentions this name.
---
 pretyping/evarsolve.ml | 35 ++++++++++++++++++++++++++---------
 1 file changed, 26 insertions(+), 9 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 13c63e9784..a03b50b72d 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -315,6 +315,7 @@ let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
 
 let free_vars_and_rels_up_alias_expansion aliases c =
   let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
+  let acc3 = ref Int.Set.empty and acc4 = ref Id.Set.empty in
   let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
   let is_in_cache depth = function
     | Rel n -> Int.Set.mem (n-depth) !cache_rel
@@ -329,8 +330,13 @@ let free_vars_and_rels_up_alias_expansion aliases c =
     | Rel _ | Var _ as ck ->
       if is_in_cache depth ck then () else begin
       put_in_cache depth ck;
-      let c = expansion_of_var aliases c in
+      let c' = expansion_of_var aliases c in
+      (if c != c' then (* expansion, hence a let-in *)
         match kind_of_term c with
+        | Var id -> acc4 := Id.Set.add id !acc4
+        | Rel n -> if n >= depth+1 then acc3 := Int.Set.add (n-depth) !acc3
+        | _ -> ());
+      match kind_of_term c' with
         | Var id -> acc2 := Id.Set.add id !acc2
         | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
         | _ -> frec (aliases,depth) c end
@@ -342,7 +348,7 @@ let free_vars_and_rels_up_alias_expansion aliases c =
           frec (aliases,depth) c
   in
   frec (aliases,0) c;
-  (!acc1,!acc2)
+  (!acc1,!acc2,!acc3,!acc4)
 
 (********************************)
 (* Managing pattern-unification *)
@@ -378,7 +384,7 @@ let get_actual_deps aliases l t =
     l
   else
     (* Probably strong restrictions coming from t being evar-closed *)
-    let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
+    let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion aliases t in
     List.filter (fun c ->
       match kind_of_term c with
       | Var id -> Id.Set.mem id fv_ids
@@ -1034,12 +1040,23 @@ let rec is_constrainable_in top force env evd k (ev,(fv_rels,fv_ids) as g) t =
   | Sort _ -> true
   | _ -> (* We don't try to be more clever *) not force || noccur_evar env evd ev t
 
-let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids as fvs) t =
-  let t = expansion_of_var aliases t in
-  match kind_of_term t with
-  | Var id -> Id.Set.mem id fv_ids
-  | Rel n -> n <= k || Int.Set.mem n fv_rels
-  | _ -> is_constrainable_in true force env evd k (ev,fvs) t
+let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t =
+  let t' = expansion_of_var aliases t in
+  if t' != t then
+    (* t is a local definition, we keep it only if appears in the list *)
+    (* of let-in variables effectively occurring on the right-hand side, *)
+    (* which is the only reason to keep it when inverting arguments *)
+    match kind_of_term t with
+    | Var id -> Id.Set.mem id let_ids
+    | Rel n -> Int.Set.mem n let_rels
+    | _ -> assert false
+  else
+    (* t is an instance for a proper variable; we filter it along *)
+    (* the free variables allowed to occur *)
+    match kind_of_term t with
+    | Var id -> Id.Set.mem id fv_ids
+    | Rel n -> n <= k || Int.Set.mem n fv_rels
+    | _ -> is_constrainable_in true force env evd k (ev,(fv_rels,fv_ids)) t
 
 exception EvarSolvedOnTheFly of evar_map * constr
 
-- 
cgit v1.2.3


From 1303e5683cb26f9dd8ed385df08d6a68b6b28fdc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Feb 2015 07:40:11 +0100
Subject: Optimizing noccur_evar wrt expansion of let-ins (fix for variant of
 #4076).

---
 pretyping/evarsolve.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index a03b50b72d..d3ab4683d8 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -178,7 +178,9 @@ let restrict_instance evd evk filter argsv =
   Filter.filter_array (Filter.compose (evar_filter evi) filter) argsv
 
 let noccur_evar env evd evk c =
-  let rec occur_rec k c = match kind_of_term c with
+  let cache = ref Int.Set.empty (* cache for let-ins *) in
+  let rec occur_rec k c =
+  match kind_of_term c with
   | Evar (evk',args' as ev') ->
       (match safe_evar_value evd ev' with
        | Some c -> occur_rec k c
@@ -186,9 +188,10 @@ let noccur_evar env evd evk c =
            if Evar.equal evk evk' then raise Occur
            else Array.iter (occur_rec k) args')
   | Rel i when i > k ->
+      if not (Int.Set.mem (i-k) !cache) then
       (match pi2 (Environ.lookup_rel (i-k) env) with
        | None -> ()
-       | Some b -> occur_rec k (lift i b))
+       | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec k (lift i b))
   | Proj (p,c) -> occur_rec k (Retyping.expand_projection env evd p c [])
   | _ -> iter_constr_with_binders succ occur_rec k c
   in
-- 
cgit v1.2.3


From 30406ca1162631ea7e0378dd8b9b3ef437c5d95d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Feb 2015 13:21:52 +0100
Subject: Still continuing cf6a68b45, d64b5766a and 2734891ab7e on integrating
 ensure_evar_independent into is_constrainable_in (a simpler approach closest
 to what existed before cf6a68b45).

---
 pretyping/evarsolve.ml | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index d3ab4683d8..f355d9a725 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1026,22 +1026,24 @@ exception CannotProject of evar_map * existential
   of subterms to eventually discard so as to be allowed to keep ti.
 *)
 
-let rec is_constrainable_in top force env evd k (ev,(fv_rels,fv_ids) as g) t =
-  let f,args = decompose_app_vect t in
+let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t =
+  let f,args2 = decompose_app_vect t in
+  let f,args1 = decompose_app_vect (whd_evar evd f) in
+  let args = Array.append args1 args2 in
   match kind_of_term f with
   | Construct ((ind,_),u) ->
     let n = Inductiveops.inductive_nparams ind in
     if n > Array.length args then true (* We don't try to be more clever *)
     else
       let params = fst (Array.chop n args) in
-      Array.for_all (is_constrainable_in false force env evd k g) params
-  | Ind _ -> Array.for_all (is_constrainable_in false force env evd k g) args
-  | Prod (na,t1,t2) -> is_constrainable_in false force env evd k g t1 && is_constrainable_in false force (push_rel (na,None,t1) env) evd k g t2
-  | Evar (ev',_) -> top || not (force || Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
+      Array.for_all (is_constrainable_in false evd k g) params
+  | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args
+  | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2
+  | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
   | Sort _ -> true
-  | _ -> (* We don't try to be more clever *) not force || noccur_evar env evd ev t
+  | _ -> (* We don't try to be more clever *) true
 
 let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t =
   let t' = expansion_of_var aliases t in
@@ -1059,7 +1061,7 @@ let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_r
     match kind_of_term t with
     | Var id -> Id.Set.mem id fv_ids
     | Rel n -> n <= k || Int.Set.mem n fv_rels
-    | _ -> is_constrainable_in true force env evd k (ev,(fv_rels,fv_ids)) t
+    | _ -> (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t
 
 exception EvarSolvedOnTheFly of evar_map * constr
 
-- 
cgit v1.2.3


From f17fa1daa613a4f86e6bdbf51ed7e758f158f938 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 25 Feb 2015 16:25:20 +0100
Subject: STM: proof state also includes meta counters

Workers send back incomplete system states (only the proof part).
Such part must include the meta/evar counter.
---
 pretyping/evarutil.ml  | 8 ++++++--
 pretyping/evarutil.mli | 3 +++
 2 files changed, 9 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 0b8cbff36c..201a16ebeb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -212,9 +212,11 @@ let whd_head_evar sigma c =
 (* Creating new metas *)
 (**********************)
 
+let meta_counter_summary_name = "meta counter"
+
 (* Generator of metavariables *)
 let new_meta =
-  let meta_ctr = Summary.ref 0 ~name:"meta counter" in
+  let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
   fun () -> incr meta_ctr; !meta_ctr
 
 let mk_new_meta () = mkMeta(new_meta())
@@ -241,9 +243,11 @@ let make_pure_subst evi args =
 (* Creating new evars *)
 (**********************)
 
+let evar_counter_summary_name = "evar counter"
+
 (* Generator of existential names *)
 let new_untyped_evar =
-  let evar_ctr = Summary.ref 0 ~name:"evar counter" in
+  let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
   fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
 
 (*------------------------------------*
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 92a3984ba6..49036798e6 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -243,3 +243,6 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b ->
 
 val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
+
+val meta_counter_summary_name : string
+val evar_counter_summary_name : string
-- 
cgit v1.2.3