From 43104a0b94e42fb78764b5d1365ca1e85a158508 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 10 Sep 2016 11:31:01 +0200
Subject: Fixing #5077 (failure on typing a fixpoint with evars in its type).

Typing.type_of was using conversion for types of fixpoints while it
could have used unification.
---
 pretyping/pretyping.ml | 17 +----------------
 pretyping/typing.ml    | 12 +++++++++++-
 pretyping/typing.mli   |  5 +++++
 3 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d6f8f0de5f..2e164e540a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -267,21 +267,6 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
 (* 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 *)
-(* Semble exagérement fort *)
-(* Faudra préférer une unification entre les types de toutes les clauses *)
-(* et autoriser des ? à rester dans le résultat de l'unification *)
-
-let evar_type_fixpoint loc env evdref lna lar vdefj =
-  let lt = Array.length vdefj in
-    if Int.equal (Array.length lar) lt then
-      for i = 0 to lt-1 do
-        if not (e_cumul env evdref (vdefj.(i)).uj_type
-		  (lift lt lar.(i))) then
-          error_ill_typed_rec_body_loc loc env !evdref
-            i lna vdefj lar
-      done
-
 (* coerce to tycon if any *)
 let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function
   | None -> j
@@ -579,7 +564,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	    { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
 	      uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
         ctxtv vdef in
-      evar_type_fixpoint loc env evdref names ftys vdefj;
+      Typing.check_type_fixpoint loc env evdref names ftys vdefj;
       let ftys = Array.map (nf_evar !evdref) ftys in
       let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
       let fixj = match fixkind with
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index eb16628b10..bb3f19859f 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -126,6 +126,16 @@ let e_judge_of_case env evdref ci pj cj lfj =
   { uj_val  = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
     uj_type = rslty }
 
+let check_type_fixpoint loc env evdref lna lar vdefj =
+  let lt = Array.length vdefj in
+    if Int.equal (Array.length lar) lt then
+      for i = 0 to lt-1 do
+        if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type
+		  (lift lt lar.(i))) then
+          Pretype_errors.error_ill_typed_rec_body_loc loc env !evdref
+            i lna vdefj lar
+      done
+
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
   let pj = Retyping.get_judgment_of env sigma p in
@@ -263,7 +273,7 @@ and execute_recdef env evdref (names,lar,vdef) =
   let env1 = push_rec_types (names,lara,vdef) env in
   let vdefj = execute_array env1 evdref vdef in
   let vdefv = Array.map j_val vdefj in
-  let _ = type_fixpoint env1 names lara vdefj in
+  let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in
   (names,lara,vdefv)
 
 and execute_array env evdref = Array.map (execute env evdref)
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index dafd75231a..22cb7f3b93 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -39,3 +39,8 @@ val solve_evars : env -> evar_map ref -> constr -> constr
 (** (first constr is term to match, second is return predicate) *)
 val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr ->
   unit
+
+(** Raise an error message if bodies have types not unifiable with the
+    expected ones *)
+val check_type_fixpoint : Loc.t -> env -> evar_map ref ->
+  Names.Name.t array -> types array -> unsafe_judgment array -> unit
-- 
cgit v1.2.3


From 74f8381ed943f1e786b32c49fb31f14fd488dc9c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 10 Sep 2016 11:37:21 +0200
Subject: Test for #5077.

---
 test-suite/bugs/closed/5077.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/closed/5077.v

diff --git a/test-suite/bugs/closed/5077.v b/test-suite/bugs/closed/5077.v
new file mode 100644
index 0000000000..7e7f2c3737
--- /dev/null
+++ b/test-suite/bugs/closed/5077.v
@@ -0,0 +1,8 @@
+(* Testing robustness of typing for a fixpoint with evars in its type *)
+
+Inductive foo (n : nat) : Type := .
+Definition foo_denote {n} (x : foo n) : Type := match x with end.
+
+Definition baz : forall n (x : foo n), foo_denote x.
+refine (fix go n (x : foo n) : foo_denote x := _).
+Abort.  
-- 
cgit v1.2.3


From 90e5945e1666540bc18e7a9b831d136041f4e487 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 12 Sep 2016 17:22:03 +0200
Subject: Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.

---
 interp/notation_ops.ml           | 3 ++-
 test-suite/output/Notations2.out | 2 ++
 test-suite/output/Notations2.v   | 5 +++++
 3 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 5abc7794bd..ec4b2e9386 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -577,7 +577,8 @@ let rec alpha_var id1 id2 = function
 
 let add_env alp (sigma,sigmalist,sigmabinders) var v =
   (* Check that no capture of binding variables occur *)
-  if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match;
+  if not (Id.equal ldots_var var) &&
+     List.exists (fun (id,_) -> occur_glob_constr id v) alp then raise No_match;
   (* TODO: handle the case of multiple occs in different scopes *)
   ((var,v)::sigma,sigmalist,sigmabinders)
 
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 6ff1d38372..13ed7816d8 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -54,3 +54,5 @@ end
      : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
 exist (Q x) y conj
      : {x0 : A | Q x x0}
+{1, 2}
+     : nat -> Prop
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 4e0d135d7d..3f3945052e 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -106,3 +106,8 @@ Check fun x (H:le x 0) => exist (le x) 0 H.
 
 Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
 Check (exist (Q x) y conj).
+
+(* Check bug raised on coq-club on Sep 12, 2016 *)
+
+Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))).
+Check ({1, 2}).
-- 
cgit v1.2.3


From 2aaa58c22e37b05e3637ac7161bb464da7db054a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Sep 2016 10:22:41 +0200
Subject: Fixing test-suite after commit 43104a0b.

---
 test-suite/success/TestRefine.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index c8a8b862fa..023cb5f59d 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -53,7 +53,7 @@ Abort.
 
 Lemma essai2 : forall x : nat, x = x.
 
-Fail refine (fix f (x : nat) : x = x := _).
+refine (fix f (x : nat) : x = x := _).
 
 Restart.
 
-- 
cgit v1.2.3