From 6482ca75a39709e65de676d533b3d115ad2b1153 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 3 Jul 2015 01:14:17 +0200
Subject: Fix convertibility of primitive projections for native_compute.

Stuck primitive projections were never convertible.
---
 kernel/nativeconv.ml | 22 ++++++++++++++--------
 1 file changed, 14 insertions(+), 8 deletions(-)

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 1f8bfc984f..d0aa96fd15 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -20,11 +20,15 @@ let rec conv_val env pb lvl cu v1 v2 =
   if v1 == v2 then ()
   else
     match kind_of_value v1, kind_of_value v2 with
-    | Vaccu k1, Vaccu k2 ->
-	conv_accu env pb lvl cu k1 k2
     | Vfun f1, Vfun f2 ->
 	let v = mk_rel_accu lvl in
 	conv_val env CONV (lvl+1) cu (f1 v) (f2 v)
+    | Vfun f1, _ ->
+	conv_val env CONV lvl cu v1 (fun x -> v2 x)
+    | _, Vfun f2 ->
+	conv_val env CONV lvl cu (fun x -> v1 x) v2
+    | Vaccu k1, Vaccu k2 ->
+	conv_accu env pb lvl cu k1 k2
     | Vconst i1, Vconst i2 -> 
 	if not (Int.equal i1 i2) then raise NotConvertible
     | Vblock b1, Vblock b2 ->
@@ -40,11 +44,7 @@ let rec conv_val env pb lvl cu v1 v2 =
 	    aux lvl max b1 b2 (i+1) cu)
 	in
 	aux lvl (n1-1) b1 b2 0 cu
-    | Vfun f1, _ -> 
-	conv_val env CONV lvl cu v1 (fun x -> v2 x)
-    | _, Vfun f2 ->
-	conv_val env CONV lvl cu (fun x -> v1 x) v2
-    | _, _ -> raise NotConvertible
+    | Vaccu _, _ | Vconst _, _ | Vblock _, _ -> raise NotConvertible
 
 and conv_accu env pb lvl cu k1 k2 = 
   let n1 = accu_nargs k1 in
@@ -60,6 +60,7 @@ and conv_atom env pb lvl a1 a2 cu =
   if a1 == a2 then ()
   else
     match a1, a2 with
+    | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false
     | Arel i1, Arel i2 -> 
 	if not (Int.equal i1 i2) then raise NotConvertible
     | Aind ind1, Aind ind2 ->
@@ -104,7 +105,12 @@ and conv_atom env pb lvl a1 a2 cu =
 	conv_val env CONV lvl cu d1 d2;
 	let v = mk_rel_accu lvl in
 	conv_val env pb (lvl + 1) cu (d1 v) (d2 v)
-    | _, _ -> raise NotConvertible
+    | Aproj(p1,ac1), Aproj(p2,ac2) ->
+       if not (Constant.equal p1 p2) then raise NotConvertible
+       else conv_accu env CONV lvl cu ac1 ac2
+    | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _
+    | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _
+    | Aproj _, _ -> raise NotConvertible
 
 (* Precondition length t1 = length f1 = length f2 = length t2 *)
 and conv_fix env lvl t1 f1 t2 f2 cu =
-- 
cgit v1.2.3


From 31c7542731a62f56bd60f443a84d68813f8780a8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Jun 2015 16:39:54 +0200
Subject: Fixing bug #4265: coqdep does not handle From ... Require.

The search algorithm is not satisfactory though, as it crawls through
all known files to find the proper one. We should rather use some trie-based
data structure, but I'll leave this for a future commit.
---
 tools/coqdep.ml         | 37 +++++++++++++--------------
 tools/coqdep_common.ml  | 68 ++++++++++++++++++++++++++++++++++++-------------
 tools/coqdep_common.mli |  2 +-
 tools/coqdep_lexer.mli  |  2 +-
 tools/coqdep_lexer.mll  | 11 +++-----
 5 files changed, 74 insertions(+), 46 deletions(-)

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index f246dc69c4..ec8e983ec2 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -55,11 +55,12 @@ let sort () =
       try
 	while true do
 	  match coq_action lb with
-	    | Require sl ->
+	    | Require (from, sl) ->
 		List.iter
 		  (fun s ->
-		    try loop (Hashtbl.find vKnown s)
-		    with Not_found -> ())
+                    match search_v_known ?from s with
+                    | None -> ()
+                    | Some f -> loop f)
 		sl
 	    | _ -> ()
 	done
@@ -298,16 +299,15 @@ module DAG = DAG(struct type t = string let compare = compare end)
 (** TODO: we should share this code with Coqdep_common *)
 let treat_coq_file chan =
   let buf = Lexing.from_channel chan in
-  let deja_vu_v = ref ([]: string list list)
+  let deja_vu_v = ref ([]: (string list option * string list) list)
   and deja_vu_ml = ref ([] : string list) in
-  let mark_v_done acc str =
-    let seen = List.mem str !deja_vu_v in
+  let mark_v_done from acc str =
+    let seen = List.mem (from, str) !deja_vu_v in
     if not seen then
-      let () = addQueue deja_vu_v str in
-      try
-        let file_str = Hashtbl.find vKnown str in
-        (canonize file_str, !suffixe) :: acc
-      with Not_found -> acc
+      let () = addQueue deja_vu_v (from, str) in
+      match search_v_known ?from str with
+      | None -> acc
+      | Some file_str -> (canonize file_str, !suffixe) :: acc
     else acc
   in
   let rec loop acc =
@@ -316,8 +316,8 @@ let treat_coq_file chan =
     | None -> acc
     | Some action ->
       let acc = match action with
-      | Require strl ->
-        List.fold_left mark_v_done acc strl
+      | Require (from, strl) ->
+        List.fold_left (fun accu v -> mark_v_done from accu v) acc strl
       | Declare sl ->
         let declare suff dir s =
           let base = file_name s dir in
@@ -339,13 +339,12 @@ let treat_coq_file chan =
         List.fold_left decl acc sl
       | Load str ->
         let str = Filename.basename str in
-        let seen = List.mem [str] !deja_vu_v in
+        let seen = List.mem (None, [str]) !deja_vu_v in
         if not seen then
-          let () = addQueue deja_vu_v [str] in
-          try
-            let file_str = Hashtbl.find vKnown [str] in
-            (canonize file_str, ".v") :: acc
-          with Not_found -> acc
+          let () = addQueue deja_vu_v (None, [str]) in
+          match search_v_known [str] with
+          | None -> acc
+          | Some file_str -> (canonize file_str, ".v") :: acc
         else acc
       | AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *)
       in
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 743853738a..0868c9e117 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -86,9 +86,9 @@ let vAccu   = ref ([] : (string * string) list)
 
 let addQueue q v = q := v :: !q
 
-let safe_hash_add cmp clq q (k,v) =
+let safe_hash_add cmp clq q (k, (v, b)) =
   try
-    let v2 = Hashtbl.find q k in
+    let (v2, _) = Hashtbl.find q k in
     if not (cmp v v2) then
       let rec add_clash = function
           (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl
@@ -96,8 +96,8 @@ let safe_hash_add cmp clq q (k,v) =
         | [] -> [(k,[v;v2])] in
       clq := add_clash !clq;
       (* overwrite previous bindings, as coqc does *)
-      Hashtbl.add q k v
-  with Not_found -> Hashtbl.add q k v
+      Hashtbl.add q k (v, b)
+  with Not_found -> Hashtbl.add q k (v, b)
 
 (** Files found in the loadpaths.
     For the ML files, the string is the basename without extension.
@@ -126,9 +126,37 @@ let add_mli_known, iter_mli_known, search_mli_known = mkknown ()
 let add_mllib_known, _, search_mllib_known = mkknown ()
 let add_mlpack_known, _, search_mlpack_known = mkknown ()
 
-let vKnown = (Hashtbl.create 19 : (string list, string) Hashtbl.t)
+let vKnown = (Hashtbl.create 19 : (string list, string * bool) Hashtbl.t)
+(** The associated boolean is true if this is a root path. *)
 let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t)
 
+let get_prefix p l =
+  let rec drop_prefix_rec = function
+    | (h1::tp, h2::tl) when h1 = h2 -> drop_prefix_rec (tp,tl)
+    | ([], tl) -> Some tl
+    | _ -> None
+  in
+  drop_prefix_rec (p, l)
+
+exception Found of string
+
+let search_v_known ?from s = match from with
+| None -> fst (Hashtbl.find vKnown s)
+| Some from ->
+  let iter logpath (phys_dir, root) =
+    if root then match get_prefix from logpath with
+    | None -> ()
+    | Some rem ->
+      match get_prefix (List.rev s) (List.rev rem) with
+      | None -> ()
+      | Some _ -> raise (Found phys_dir)
+  in
+  try Hashtbl.iter iter vKnown; raise Not_found
+  with Found s -> s
+
+let search_v_known ?from s =
+  try Some (search_v_known ?from s) with Not_found -> None
+
 let clash_v = ref ([]: (string list * string list) list)
 
 let error_cannot_parse s (i,j) =
@@ -163,9 +191,11 @@ let warning_clash file dir =
       eprintf "%s and %s; used the latter)\n" d2 d1
   | _ -> assert false
 
-let safe_assoc verbose file k =
+let safe_assoc from verbose file k =
   if verbose && List.mem_assoc k !clash_v then warning_clash file k;
-  Hashtbl.find vKnown k
+  match search_v_known ?from k with
+  | None -> raise Not_found
+  | Some path -> path
 
 let absolute_dir dir =
   let current = Sys.getcwd () in
@@ -309,18 +339,18 @@ let rec traite_fichier_Coq suffixe verbose f =
   try
     let chan = open_in f in
     let buf = Lexing.from_channel chan in
-    let deja_vu_v = ref ([]: string list list)
+    let deja_vu_v = ref ([]: (string list option * string list) list)
     and deja_vu_ml = ref ([] : string list) in
     try
       while true do
       	let tok = coq_action buf in
 	match tok with
-	  | Require strl ->
+	  | Require (from, strl) ->
 	      List.iter (fun str ->
-		if not (List.mem str !deja_vu_v) then begin
-	          addQueue deja_vu_v str;
+		if not (List.mem (from, str) !deja_vu_v) then begin
+	          addQueue deja_vu_v (from, str);
                   try
-                    let file_str = safe_assoc verbose f str in
+                    let file_str = safe_assoc from verbose f str in
                     printf " %s%s" (canonize file_str) suffixe
                   with Not_found ->
 		    if verbose && not (Hashtbl.mem coqlibKnown str) then
@@ -349,10 +379,10 @@ let rec traite_fichier_Coq suffixe verbose f =
 	      in List.iter decl sl
 	  | Load str ->
 	      let str = Filename.basename str in
-	      if not (List.mem [str] !deja_vu_v) then begin
-	        addQueue deja_vu_v [str];
+	      if not (List.mem (None, [str]) !deja_vu_v) then begin
+	        addQueue deja_vu_v (None, [str]);
                 try
-                  let file_str = Hashtbl.find vKnown [str] in
+                  let (file_str, _) = Hashtbl.find vKnown [str] in
                   let canon = canonize file_str in
                   printf " %s.v" canon;
                   traite_fichier_Coq suffixe true (canon ^ ".v")
@@ -441,9 +471,11 @@ let add_known recur phys_dir log_dir f =
     | (basename,".v") ->
 	let name = log_dir@[basename] in
 	let file = phys_dir//basename in
-	let paths = if recur then suffixes name else [name] in
-	List.iter
-	  (fun n -> safe_hash_add compare_file clash_v vKnown (n,file)) paths
+	let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in
+	if recur then
+          let paths = List.tl (suffixes name) in
+          let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in
+          List.iter iter paths
     | (basename,".vo") when not(!option_boot) ->
         let name = log_dir@[basename] in
 	let paths = if recur then suffixes name else [name] in
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 71b96ca0ee..23619d1e60 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -31,7 +31,7 @@ val iter_mli_known : (string -> dir -> unit) -> unit
 val search_mli_known : string -> dir option
 val add_mllib_known : string -> dir -> string -> unit
 val search_mllib_known : string -> dir option
-val vKnown : (string list, string) Hashtbl.t
+val search_v_known : ?from:string list -> string list -> string option
 val coqlibKnown : (string list, unit) Hashtbl.t
 val file_name : string -> string option -> string
 val escape : string -> string
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
index c7b9c9a0a8..84c9ba798b 100644
--- a/tools/coqdep_lexer.mli
+++ b/tools/coqdep_lexer.mli
@@ -11,7 +11,7 @@ type mL_token = Use_module of string
 type qualid = string list
 
 type coq_token =
-    Require of qualid list
+    Require of qualid option * qualid list
   | Declare of string list
   | Load of string
   | AddLoadPath of string
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 5692e5b45f..291bc55fbe 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -16,7 +16,7 @@
   type qualid = string list
 
   type coq_token =
-    | Require of qualid list
+    | Require of qualid option * qualid list
     | Declare of string list
     | Load of string
     | AddLoadPath of string
@@ -270,12 +270,9 @@ and require_file = parse
         module_names := [coq_qual_id_tail lexbuf];
         let qid = coq_qual_id_list lexbuf in
         parse_dot lexbuf;
-	match !from_pre_ident with
-	  None ->
-          Require qid
-	| Some from ->
-	  (from_pre_ident := None ;
-	   Require (List.map (fun x -> from @ x) qid)) }
+        let from = !from_pre_ident in
+        from_pre_ident := None;
+        Require (from, qid) }
   | eof
       { syntax_error lexbuf }
   | _
-- 
cgit v1.2.3


From a51cce369b9c634a93120092d4c7685a242d55b1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 4 Jul 2015 14:22:08 +0200
Subject: Fix handling of primitive projections in VM.

I'm pushing this patch now because the previous treatment of such projections
in the VM was already unsound. It should however be carefully reviewed.
---
 kernel/byterun/coq_fix_code.c |  2 +-
 kernel/byterun/coq_instruct.h |  1 +
 kernel/byterun/coq_interp.c   | 28 ++++++++++++++++++++++++++--
 kernel/byterun/coq_values.h   |  9 +++++----
 kernel/cbytecodes.ml          |  6 ++++++
 kernel/cbytecodes.mli         |  3 +++
 kernel/cbytegen.ml            | 14 ++++++--------
 kernel/cemitcodes.ml          |  1 +
 kernel/csymtable.ml           |  7 +++++--
 kernel/term_typing.ml         | 20 ++++++++++++++++++--
 kernel/vconv.ml               | 17 ++++++++++++-----
 kernel/vm.ml                  | 22 ++++++++++++++--------
 kernel/vm.mli                 |  1 +
 pretyping/inductiveops.ml     |  9 +++++++++
 pretyping/inductiveops.mli    |  2 ++
 pretyping/pretyping.mllib     |  2 +-
 pretyping/retyping.ml         |  9 ++-------
 pretyping/vnorm.ml            |  4 ++++
 18 files changed, 117 insertions(+), 40 deletions(-)

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 1be3e65113..29e33d349b 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -60,7 +60,7 @@ void init_arity () {
     arity[BRANCH]=arity[ISCONST]= 1;
   /* instruction with two operands */
   arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
-  arity[ARECONST]=2;
+  arity[ARECONST]=arity[PROJ]=2;
   /* instruction with four operands */ 
   arity[MAKESWITCHBLOCK]=4;
   /* instruction with arbitrary operands */
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 9cbf4077e2..8c5ab0ecbd 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -36,6 +36,7 @@ enum instructions {
   SWITCH, PUSHFIELDS, 
   GETFIELD0, GETFIELD1, GETFIELD, 
   SETFIELD0, SETFIELD1, SETFIELD,
+  PROJ,
   CONST0, CONST1, CONST2, CONST3, CONSTINT,
   PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
   ACCUMULATE,
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index ddbde9d385..0a121dc32e 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -878,8 +878,32 @@ value coq_interprete
 	caml_modify(&Field(accu, *pc),*sp);
 	sp++; pc++;
 	Next;
-      }	
-   
+      }
+
+
+      Instruct(PROJ){
+	print_instr("PROJ");
+	if (Is_accu (accu)) {
+	  /* Skip over the index of projected field */
+	  pc++;
+	  /* Save the argument on the stack */
+	  *--sp = accu;
+	  /* Create atom */
+	  Alloc_small(accu, 2, ATOM_PROJ_TAG);
+	  Field(accu, 0) = Field(coq_global_data, *pc);
+	  Field(accu, 1) = sp[0];
+	  sp[0] = accu;
+	  /* Create accumulator */
+	  Alloc_small(accu, 2, Accu_tag);
+	  Code_val(accu) = accumulate;
+	  Field(accu,1) = *sp++;
+	} else {
+	    accu = Field(accu, *pc++);
+	}
+	pc++;
+	Next;
+      }
+
 /* Integer constants */
 
       Instruct(CONST0){
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 1bf493e2c0..1590a2141d 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -22,10 +22,11 @@
 #define ATOM_ID_TAG 0
 #define ATOM_IDDEF_TAG 1
 #define ATOM_INDUCTIVE_TAG 2
-#define ATOM_FIX_TAG 3
-#define ATOM_SWITCH_TAG 4
-#define ATOM_COFIX_TAG 5
-#define ATOM_COFIXEVALUATED_TAG 6
+#define ATOM_PROJ_TAG 3
+#define ATOM_FIX_TAG 4
+#define ATOM_SWITCH_TAG 5
+#define ATOM_COFIX_TAG 6
+#define ATOM_COFIXEVALUATED_TAG 7
 
 
 
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 93fd61f02a..3271ac1458 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -31,6 +31,7 @@ let last_variant_tag = 245
 type structured_constant =
   | Const_sorts of sorts
   | Const_ind of pinductive
+  | Const_proj of Constant.t
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
 
@@ -81,6 +82,8 @@ type instruction =
   | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
+  | Kproj of int * Constant.t  (* index of the projected argument,
+                                           name of projection *)
 (* spiwack: instructions concerning integers *)
   | Kbranch of Label.t                  (* jump to label *)
   | Kaddint31                           (* adds the int31 in the accu
@@ -167,6 +170,7 @@ let pp_sort s =
 let rec pp_struct_const = function
   | Const_sorts s -> pp_sort s
   | Const_ind ((mind, i), u) -> pr_mind mind ++ str"#" ++ int i
+  | Const_proj p -> Constant.print p
   | Const_b0 i -> int i
   | Const_bn (i,t) ->
      int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)
@@ -228,6 +232,8 @@ let rec pp_instr i =
 
   | Kbranch lbl -> str "branch " ++ pp_lbl lbl
 
+  | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p
+
   | Kaddint31 -> str "addint31"
   | Kaddcint31 -> str "addcint31"
   | Kaddcarrycint31 -> str "addcarrycint31"
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index d9998c89e8..745ef311b0 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -25,6 +25,7 @@ val last_variant_tag : tag
 type structured_constant =
   | Const_sorts of sorts
   | Const_ind of pinductive
+  | Const_proj of Constant.t
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
 
@@ -72,6 +73,8 @@ type instruction =
   | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
+  | Kproj of int * Constant.t  (** index of the projected argument,
+                                            name of projection *)
 
 (** spiwack: instructions concerning integers *)
   | Kbranch of Label.t                  (** jump to label, is it needed ? *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index ac46dc5833..d5435f0c37 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -540,14 +540,12 @@ let rec compile_constr reloc c sz cont =
   match kind_of_term c with
   | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta"
   | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar"
-  | Proj (p,c) -> 
-    (* compile_const reloc p [|c|] sz cont *)
-    let kn = Projection.constant p in
-    let cb = lookup_constant kn !global_env in
-      (* TODO: better representation of projections *)
-    let pb = Option.get cb.const_proj in
-    let args = Array.make pb.proj_npars mkProp in
-      compile_const reloc kn Univ.Instance.empty (Array.append args [|c|]) sz cont
+  | Proj (p,c) ->
+     let kn = Projection.constant p in
+     let cb = lookup_constant kn !global_env in
+     let pb = Option.get cb.const_proj in
+     let n = pb.proj_arg in
+     compile_constr reloc c sz (Kproj (n,kn) :: cont)
 
   | Cast(c,_,_) -> compile_constr reloc c sz cont
 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 2535a64d3c..0d9334a50c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -225,6 +225,7 @@ let emit_instr = function
       if n <= 1 then out (opSETFIELD0+n)
       else (out opSETFIELD;out_int n)
   | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
+  | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p)
   (* spiwack *)
   | Kbranch lbl -> out opBRANCH; out_label lbl
   | Kaddint31 -> out opADDINT31
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 49ab68beae..8fd90ec364 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -60,6 +60,8 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with
 | Const_sorts _, _ -> false
 | Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2
 | Const_ind _, _ -> false
+| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
+| Const_proj _, _ -> false
 | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
 | Const_b0 _, _ -> false
 | Const_bn (t1, a1), Const_bn (t2, a2) ->
@@ -71,11 +73,12 @@ let rec hash_structured_constant c =
   match c with
   | Const_sorts s -> combinesmall 1 (Sorts.hash s)
   | Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u))
-  | Const_b0 t -> combinesmall 3 (Int.hash t)
+  | Const_proj p -> combinesmall 3 (Constant.hash p)
+  | Const_b0 t -> combinesmall 4 (Int.hash t)
   | Const_bn (t, a) ->
     let fold h c = combine h (hash_structured_constant c) in
     let h = Array.fold_left fold 0 a in
-    combinesmall 4 (combine (Int.hash t) h)
+    combinesmall 5 (combine (Int.hash t) h)
 
 module SConstTable = Hashtbl.Make (struct
   type t = structured_constant
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a316b4492b..83e566041f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -251,7 +251,24 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
 	match proj with
 	| None -> compile_constant_body env def
 	| Some pb ->
-	   compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))
+	(* The compilation of primitive projections is a bit tricky, because
+           they refer to themselves (the body of p looks like fun c =>
+           Proj(p,c)). We break the cycle by building an ad-hoc compilation
+           environment. A cleaner solution would be that kernel projections are
+           simply Proj(i,c) with i an int and c a constr, but we would have to
+           get rid of the compatibility layer. *)
+	   let cb =
+	     { const_hyps = hyps;
+	       const_body = def;
+	       const_type = typ;
+	       const_proj = proj;
+	       const_body_code = None;
+	       const_polymorphic = poly;
+	       const_universes = univs;
+	       const_inline_code = inline_code }
+	   in
+	   let env = add_constant kn cb env in
+	   compile_constant_body env def
       in Option.map Cemitcodes.from_val res
   in
   { const_hyps = hyps;
@@ -263,7 +280,6 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
     const_universes = univs;
     const_inline_code = inline_code }
 
-
 (*s Global and local constant declaration. *)
 
 let translate_constant env kn ce =
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 1c31cc0414..a03a67db8b 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -18,8 +18,8 @@ let compare_zipper z1 z2 =
   match z1, z2 with
   | Zapp args1, Zapp args2 -> Int.equal (nargs args1) (nargs args2)
   | Zfix(f1,args1), Zfix(f2,args2) ->  Int.equal (nargs args1) (nargs args2)
-  | Zswitch _, Zswitch _ -> true
-  | _ , _ -> false
+  | Zswitch _, Zswitch _ | Zproj _, Zproj _ -> true
+  | Zapp _ , _ | Zfix _, _ | Zswitch _, _ | Zproj _, _ -> false
 
 let rec compare_stack stk1 stk2 =
   match stk1, stk2 with
@@ -81,7 +81,10 @@ and conv_whd env pb k whd1 whd2 cu =
       conv_whd env pb k whd1 (force_whd v stk) cu
   | Vatom_stk(Aiddef(_,v),stk), _ ->
       conv_whd env pb k (force_whd v stk) whd2 cu
-  | _, _ -> raise NotConvertible
+
+  | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _  | Vconstr_const _, _
+  | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
+
 
 and conv_atom env pb k a1 stk1 a2 stk2 cu =
   match a1, a2 with
@@ -110,7 +113,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
       conv_whd env pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
   | _, Aiddef(ik2,v2) ->
       conv_whd env pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
-  | _, _ -> raise NotConvertible
+  | Aind _, _ | Aid _, _ -> raise NotConvertible
 
 and conv_stack env k stk1 stk2 cu =
   match stk1, stk2 with
@@ -131,7 +134,11 @@ and conv_stack env k stk1 stk2 cu =
 	done;
 	conv_stack env k stk1 stk2 !rcu
       else raise NotConvertible
-  | _, _ -> raise NotConvertible
+  | Zproj p1 :: stk1, Zproj p2 :: stk2 ->
+    if Constant.equal p1 p2 then conv_stack env k stk1 stk2 cu
+    else raise NotConvertible
+  | [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _
+  | Zproj _ :: _, _ -> raise NotConvertible
 
 and conv_fun env pb k f1 f2 cu =
   if f1 == f2 then cu
diff --git a/kernel/vm.ml b/kernel/vm.ml
index d4bf461b39..a822f92eb3 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -127,10 +127,11 @@ type vswitch = {
 (* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ]            *)
 (*   - representation of [accu] : tag_[....]                              *)
 (*     -- tag <= 2 : encoding atom type (sorts, free vars, etc.)          *)
-(*     -- 3_[accu|fix_app] : a fixpoint blocked by an accu                *)
-(*     -- 4_[accu|vswitch] : a match blocked by an accu                   *)
-(*     -- 5_[fcofix]       : a cofix function                             *)
-(*     -- 6_[fcofix|val]   : a cofix function, val represent the value    *)
+(*     -- 3_[accu|proj name] : a projection blocked by an accu            *)
+(*     -- 4_[accu|fix_app] : a fixpoint blocked by an accu                *)
+(*     -- 5_[accu|vswitch] : a match blocked by an accu                   *)
+(*     -- 6_[fcofix]       : a cofix function                             *)
+(*     -- 7_[fcofix|val]   : a cofix function, val represent the value    *)
 (*        of the function applied to arg1 ... argn                        *)
 (* The [arguments] type, which is abstracted as an array, represents :    *)
 (*          tag[ _ | _ |v1|... | vn]                                      *)
@@ -149,6 +150,7 @@ type zipper =
   | Zapp of arguments
   | Zfix of vfix*arguments  (* Possibly empty *)
   | Zswitch of vswitch
+  | Zproj of Constant.t (* name of the projection *)
 
 type stack = zipper list
 
@@ -176,15 +178,18 @@ let rec whd_accu a stk =
   match Obj.tag at with
   | i when i <= 2 ->
       Vatom_stk(Obj.magic at, stk)
-  | 3 (* fix_app tag *) ->
+  | 3 (* proj tag *) ->
+     let zproj = Zproj (Obj.obj (Obj.field at 0)) in
+     whd_accu (Obj.field at 1) (zproj :: stk)
+  | 4 (* fix_app tag *) ->
       let fa = Obj.field at 1 in
       let zfix  =
 	Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
       whd_accu (Obj.field at 0) (zfix :: stk)
-  | 4 (* switch tag  *) ->
+  | 5 (* switch tag  *) ->
       let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
       whd_accu (Obj.field at 0) (zswitch :: stk)
-  | 5 (* cofix_tag *) ->
+  | 6 (* cofix_tag *) ->
       let vcfx = Obj.obj (Obj.field at 0) in
       let to_up = Obj.obj a in
       begin match stk with
@@ -192,7 +197,7 @@ let rec whd_accu a stk =
       | [Zapp args] -> Vcofix(vcfx, to_up, Some args)
       | _           -> assert false
       end
-  | 6 (* cofix_evaluated_tag *) ->
+  | 7 (* cofix_evaluated_tag *) ->
       let vcofix = Obj.obj (Obj.field at 0) in
       let res = Obj.obj a in
       begin match stk with
@@ -289,6 +294,7 @@ let rec obj_of_str_const str =
   match str with
   | Const_sorts s -> Obj.repr (Vsort s)
   | Const_ind ind -> obj_of_atom (Aind ind)
+  | Const_proj p -> Obj.repr p
   | Const_b0 tag -> Obj.repr tag
   | Const_bn(tag, args) ->
       let len = Array.length args in
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 5190356828..d31448ee13 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -34,6 +34,7 @@ type zipper =
   | Zapp of arguments
   | Zfix of vfix * arguments  (** might be empty *)
   | Zswitch of vswitch
+  | Zproj of Constant.t (* name of the projection *)
 
 type stack = zipper list
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index dfdc24d480..90aa8000a8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -584,6 +584,15 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
         env evdref scl ar.template_level (ctx,ar.template_param_levels) in
       !evdref, mkArity (List.rev ctx,scl)
 
+let type_of_projection_knowing_arg env sigma p c ty =
+  let IndType(pars,realargs) =
+    try find_rectype env sigma ty
+    with Not_found ->
+      raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type")
+  in
+  let (_,u), pars = dest_ind_family pars in
+  substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u))
+
 (***********************************************)
 (* Guard condition *)
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7959759a3f..757599a3ce 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -126,6 +126,8 @@ val allowed_sorts : env -> inductive -> sorts_family list
 (** Primitive projections *)
 val projection_nparams : projection -> int
 val projection_nparams_env : env -> projection -> int
+val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
+  constr -> types -> types
 
 (** Extract information from an inductive family *)
 
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 25d17c7c9f..a644e3d107 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -3,8 +3,8 @@ Termops
 Namegen
 Evd
 Reductionops
-Vnorm
 Inductiveops
+Vnorm
 Arguments_renaming
 Nativenorm
 Retyping
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index a56861c683..743bc3b19b 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -127,13 +127,8 @@ let retype ?(polyprop=true) sigma =
         strip_outer_cast
           (subst_type env sigma (type_of env f) (Array.to_list args))
     | Proj (p,c) -> 
-       let Inductiveops.IndType(pars,realargs) =
-	 let ty = type_of env c in
-           try Inductiveops.find_rectype env sigma ty
-           with Not_found -> retype_error BadRecursiveType
-       in
-       let (_,u), pars = dest_ind_family pars in
-	 substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u))
+       let ty = type_of env c in
+       Inductiveops.type_of_projection_knowing_arg env sigma p c ty
     | Cast (c,_, t) -> t
     | Sort _ | Prod _ -> mkSort (sort_of env cstr)
 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 8198db1b8a..af640d7f34 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -216,6 +216,10 @@ and nf_stk env c t stk  =
       let tcase = build_case_type dep p realargs c in
       let ci = case_info sw in
       nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
+  | Zproj p :: stk ->
+     let p' = Projection.make p true in
+     let ty = Inductiveops.type_of_projection_knowing_arg env Evd.empty p' c t in
+     nf_stk env (mkProj(p',c)) ty stk
 
 and nf_predicate env ind mip params v pT =
   match whd_val v, kind_of_term pT with
-- 
cgit v1.2.3


From 8a71148e8068c67c5b7d9b9b0f00ab5de5bf03b7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 30 Jun 2015 16:59:19 +0200
Subject: More precise rewording about asymmetric patterns.

---
 CHANGES | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/CHANGES b/CHANGES
index 9172195960..050d3e999f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -163,10 +163,11 @@ Specification Language
 - Constructors in pattern-matching patterns now respect the same rules
   regarding implicit arguments than in applicative position. The old
   behavior can be recovered by the command "Set Asymmetric
-  Patterns". As a side effect, Much more notations can be used in
-  patterns. Considering that the pattern language is rich enough like
-  that, definitions are now always forbidden in patterns. (source of
-  incompatibilities for definitions that delta-reduce to a constructor)
+  Patterns". As a side effect, notations for constructors explicitly
+  mentioning non-implicit parameters can now be used in patterns.
+  Considering that the pattern language is already rich enough, binding
+  local definitions is however now forbidden in patterns (source of
+  incompatibilities for local definitions that delta-reduce to a constructor).
 - Type inference algorithm now granting opacity of constants. This might also
   affect behavior of tactics (source of incompatibilities, solvable by
   re-declaring transparent constants which were set opaque).
-- 
cgit v1.2.3


From 7df4e7d5fb011ff4dbb26884bb80ece20950b178 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 5 Jul 2015 19:08:17 +0200
Subject: Fixing documentation (see Maxime's mail on coqdev, July 3).

---
 kernel/declarations.mli | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 27c1c3f3f0..c1c19a757c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -142,12 +142,10 @@ type one_inductive_body = {
     mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
 
     mind_consnrealargs : int array;
- (** Number of expected proper arguments of the constructors (w/o params)
-    (not used in the kernel) *)
+ (** Number of expected proper arguments of the constructors (w/o params) *)
 
     mind_consnrealdecls : int array;
- (** Length of the signature of the constructors (with let, w/o params)
-    (not used in the kernel) *)
+ (** Length of the signature of the constructors (with let, w/o params) *)
 
     mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
 
-- 
cgit v1.2.3


From 2face8d77628ded64f7d0a824f4b377694b9d7fd Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 6 Jul 2015 15:22:20 +0200
Subject: Test case for #4203, fixed by commit a51cce36.

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

diff --git a/test-suite/bugs/closed/4203.v b/test-suite/bugs/closed/4203.v
new file mode 100644
index 0000000000..076a3c3d68
--- /dev/null
+++ b/test-suite/bugs/closed/4203.v
@@ -0,0 +1,19 @@
+Set Primitive Projections.
+
+Record ops {T:Type} := { is_ok : T -> Prop; constant : T }.
+Arguments ops : clear implicits.
+
+Record ops_ok {T} (Ops:ops T) := { constant_ok : is_ok Ops (constant Ops) }.
+
+Definition nat_ops : ops nat := {| is_ok := fun n => n = 1; constant := 1 |}.
+Definition nat_ops_ok : ops_ok nat_ops.
+Proof.
+  split. cbn. apply eq_refl.
+Qed.
+
+Definition t := Eval lazy in constant_ok nat_ops nat_ops_ok.
+Definition t' := Eval vm_compute in constant_ok nat_ops nat_ops_ok.
+Definition t'' := Eval native_compute in constant_ok nat_ops nat_ops_ok.
+
+Check (eq_refl t : t = t').
+Check (eq_refl t : t = t'').
\ No newline at end of file
-- 
cgit v1.2.3