From 71def2f885989376c8c2940d37f7fc407ed0a4c5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Feb 2015 11:59:04 +0100
Subject: Fixing occur-check which was too strong in unification.ml.

---
 pretyping/unification.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 203b1ec8a6..99c20ef6ce 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -673,6 +673,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
               (sigma,(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst,
               evarsubst)
 	    else error_cannot_unify_local curenv sigma (m,n,cM)
+	| Evar (evk,_ as ev), Evar (evk',_)
+            when not (Evar.Set.mem evk flags.frozen_evars)
+              && Evar.equal evk evk' ->
+	    sigma,metasubst,((curenv,ev,cN)::evarsubst)
 	| Evar (evk,_ as ev), _
             when not (Evar.Set.mem evk flags.frozen_evars) 
 	      && not (occur_evar evk cN) ->
@@ -1673,11 +1677,13 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
 		 matchrec t
 	       with ex when precatchable_exception ex ->
 		 matchrec c)
+
           | Lambda (_,t,c) ->
 	      (try
 		 matchrec t
 	       with ex when precatchable_exception ex ->
 		 matchrec c)
+
           | _ -> error "Match_subterm"))
   in
   try matchrec cl
-- 
cgit v1.2.3


From 06ad2a73251f38c59c43c03a0edca34d5ef3dd8e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Feb 2015 12:43:01 +0100
Subject: Fixing rewrite/subst when the subterm to rewrite is argument of an
 Evar.

This was broken by the attempt to use the same algorithm for rewriting
closed subterms than for rewriting subterms with evars: the algorithm
to find subterms (w_unify_to_subterm) did not go through evars. But
what to do when looking say, for a pattern "S ?n" in a goal "S ?x[a:=S ?y]"?
Should we unify ?x[a:=S ?y] with ?n or consider ?x as rigid and look
in the instance? If we adopt the first approach, then, what to do when
looking for "S ?n" in a goal "?x[a:=S ?y]"? Failing? Looking in the
instance? Is it normal that an evar behaves as a rigid constant when
it cannot be unified with the pattern?
---
 pretyping/unification.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 99c20ef6ce..01e1154e58 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1780,7 +1780,12 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
           try
 	    (* This is up to delta for subterms w/o metas ... *)
 	    w_unify_to_subterm env evd ~flags (strip_outer_cast op,t)
-	  with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op)
+	  with PretypeError (env,_,NoOccurrenceFound _) when
+              allow_K ||
+                (* w_unify_to_subterm does not go through evars, so
+                   the next step, which was already in <= 8.4, is
+                   needed at least for compatibility of rewrite *)
+                dependent op t -> (evd,op)
         in
 	  if not allow_K &&
             (* ensure we found a different instance *)
-- 
cgit v1.2.3


From df2f50db3703b4f7f88f00ac382c7f3f1efaceb3 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 23 Feb 2015 11:26:51 +0100
Subject: Fix some typos in comments.

---
 pretyping/pretyping.ml  | 4 ++--
 pretyping/pretyping.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e3dba232b2..0cadffa4fe 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -82,7 +82,7 @@ let search_guard loc env possible_indexes fixdefs =
        iraise (e, info));
     indexes
   else
-    (* we now search recursively amoungst all combinations *)
+    (* we now search recursively among all combinations *)
     (try
        List.iter
 	 (fun l ->
@@ -220,7 +220,7 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
   let c = if flags.expand_evars then nf_evar sigma c else c in
   sigma,c
 
-(* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 let allow_anonymous_refs = ref false
 
 (* Utilisé pour inférer le prédicat des Cases *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7d1e0c9b5b..142b54513e 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -63,7 +63,7 @@ val all_no_fail_flags : inference_flags
 
 val all_and_fail_flags : inference_flags
 
-(** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+(** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 val allow_anonymous_refs : bool ref
   
 (** Generic call to the interpreter from glob_constr to open_constr, leaving
-- 
cgit v1.2.3