Merge branch 'v8.5'

11 files changed, 36 insertions, 64 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 399fa843f1..0553a5ed7e 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -844,7 +844,6 @@ value coq_interprete
       }
 	
       Instruct(SETFIELD1){
-        int i, j, size, size_aux;
 	print_instr("SETFIELD1");
 	caml_modify(&Field(accu, 1),*sp);
        	sp++;
@@ -884,19 +883,17 @@ value coq_interprete
       Instruct(PROJ){
 	print_instr("PROJ");
 	if (Is_accu (accu)) {
+          value block;
 	  /* 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;
+	  Alloc_small(block, 2, ATOM_PROJ_TAG);
+	  Field(block, 0) = Field(coq_global_data, *pc);
+	  Field(block, 1) = accu;
 	  /* Create accumulator */
 	  Alloc_small(accu, 2, Accu_tag);
 	  Code_val(accu) = accumulate;
-	  Field(accu,1) = *sp++;
+	  Field(accu, 1) = block;
 	} else {
 	    accu = Field(accu, *pc++);
 	}
@@ -1110,7 +1107,6 @@ value coq_interprete
 	/* returns the sum plus one with a carry */
 	uint32_t s;
 	s = (uint32_t)accu + (uint32_t)*sp++ + 1;
-	value block;
         if( (uint32_t)s <= (uint32_t)accu ) {
           /* carry */
 	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
@@ -1271,7 +1267,7 @@ value coq_interprete
 
       Instruct (COMPAREINT31) {
 	/* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
-	/* assumes Inudctive _ : _ := Eq | Lt | Gt */
+	/* assumes Inductive _ : _ := Eq | Lt | Gt */
 	print_instr("COMPAREINT31");
 	if ((uint32_t)accu == (uint32_t)*sp) {
 	  accu = 1;  /* 2*0+1 */
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 416e5e5329..c9bcdc32ff 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -103,7 +103,6 @@ static int coq_vm_initialized = 0;
 
 value init_coq_vm(value unit) /* ML */
 {
-  int i;
   if (coq_vm_initialized == 1) {
     fprintf(stderr,"already open \n");fflush(stderr);}
   else {
@@ -135,7 +134,6 @@ void realloc_coq_stack(asize_t required_space)
 {
   asize_t size;
   value * new_low, * new_high, * new_sp;
-  value * p;
   size = coq_stack_high - coq_stack_low;
   do {
     size *= 2;
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 007f61b27c..528babebfc 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -21,7 +21,6 @@
 
 value coq_kind_of_closure(value v) {
   opcode_t * c;
-  int res;
   int is_app = 0;
   c = Code_val(v);
   if (Is_instruction(c, GRAB)) return Val_int(0);
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 3b01538b92..ec2c334b6f 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -82,12 +82,17 @@ let fold_strategy f { var_opacity; cst_opacity; } accu =
 let get_transp_state { var_trstate; cst_trstate } = (var_trstate, cst_trstate)
 
 (* Unfold the first constant only if it is "more transparent" than the
-   second one. In case of tie, expand the second one. *)
+   second one. In case of tie, use the recommended default. *)
 let oracle_order f o l2r k1 k2 =
   match get_strategy o f k1, get_strategy o f k2 with
-    | Expand, _ -> true
-    | Level n1, Opaque -> true
-    | Level n1, Level n2 -> n1 < n2
-    | _ -> l2r (* use recommended default *)
+  | Expand, Expand -> l2r
+  | Expand, (Opaque | Level _) -> true
+  | (Opaque | Level _), Expand -> false
+  | Opaque, Opaque -> l2r
+  | Level _, Opaque -> true
+  | Opaque, Level _ -> false
+  | Level n1, Level n2 ->
+     if Int.equal n1 n2 then l2r
+     else n1 < n2
 
 let get_strategy o = get_strategy o (fun x -> x)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 155ad79879..697f482c49 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -290,11 +290,7 @@ let typecheck_inductive env mie =
       let full_polymorphic () = 
 	let defu = Term.univ_of_sort def_level in
 	let is_natural =
-	  type_in_type env || (UGraph.check_leq (universes env') infu defu &&
-				not (is_type0m_univ defu && not is_unit)
-				  (* (~ is_type0m_univ defu \/ is_unit) (\* infu <= defu && not prop or unital *\) *)
-
-			     )
+	  type_in_type env || (UGraph.check_leq (universes env') infu defu)
 	in
 	let _ =
 	  (** Impredicative sort, always allow *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 687b740f67..98b2d6d2e9 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -481,7 +481,7 @@ and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 =
   in
   Array.equal eq_branch br1 br2
 
-(* hash_mllambda gn n env t computes the hash for t ignoring occurences of gn *)
+(* hash_mllambda gn n env t computes the hash for t ignoring occurrences of gn *)
 let rec hash_mllambda gn n env t =
   match t with
   | MLlocal ln -> combinesmall 1 (LNmap.find ln env)
@@ -979,7 +979,7 @@ let compile_prim decl cond paux =
 	let args = Array.map opt_prim_aux args in
 	app_prim (Coq_primitive(op,None)) args
 (*
-    TODO: check if this inling was useful
+    TODO: check if this inlining was useful
 	begin match op with
         | Int31lt -> 
            if Sys.word_size = 64 then
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index cb08b5058f..263befd213 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -277,7 +277,7 @@ and reduce_lapp substf lids body substa largs =
   | [], _::_ -> simplify_app substf body substa (Array.of_list largs)
 
 
-(* [occurence kind k lam]:
+(* [occurrence kind k lam]:
    If [kind] is [true] return [true] if the variable [k] does not appear in 
    [lam], return [false] if the variable appear one time and not
    under a lambda, a fixpoint, a cofixpoint; else raise Not_found.
@@ -285,7 +285,7 @@ and reduce_lapp substf lids body substa largs =
    else raise [Not_found]
 *)
 
-let rec occurence k kind lam =   
+let rec occurrence k kind lam =
   match lam with
   | Lrel (_,n) -> 
       if Int.equal n k then 
@@ -294,35 +294,35 @@ let rec occurence k kind lam =
   | Lvar _  | Lconst _  | Lproj _ | Luint _ | Lval _ | Lsort _ | Lind _
   | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> kind
   | Lprod(dom, codom) ->
-      occurence k (occurence k kind dom) codom
+      occurrence k (occurrence k kind dom) codom
   | Llam(ids,body) ->
-      let _ = occurence (k+Array.length ids) false body in kind
+      let _ = occurrence (k+Array.length ids) false body in kind
   | Llet(_,def,body) ->
-      occurence (k+1) (occurence k kind def) body
+      occurrence (k+1) (occurrence k kind def) body
   | Lapp(f, args) ->
-      occurence_args k (occurence k kind f) args
+      occurrence_args k (occurrence k kind f) args
   | Lprim(_,_,_,args) | Lmakeblock(_,_,_,args) ->
-      occurence_args k kind args
+      occurrence_args k kind args
   | Lcase(_,t,a,br) ->
-      let kind = occurence k (occurence k kind t) a in
+      let kind = occurrence k (occurrence k kind t) a in
       let r = ref kind in
       Array.iter (fun (_,ids,c) -> 
-	r := occurence (k+Array.length ids) kind c && !r) br;
+	r := occurrence (k+Array.length ids) kind c && !r) br;
       !r 
   | Lif (t, bt, bf) ->
-      let kind = occurence k kind t in
-      kind && occurence k kind bt && occurence k kind bf
+      let kind = occurrence k kind t in
+      kind && occurrence k kind bt && occurrence k kind bf
   | Lfix(_,(ids,ltypes,lbodies)) 
   | Lcofix(_,(ids,ltypes,lbodies)) ->
-      let kind = occurence_args k kind ltypes in
-      let _ = occurence_args (k+Array.length ids) false lbodies in
+      let kind = occurrence_args k kind ltypes in
+      let _ = occurrence_args (k+Array.length ids) false lbodies in
       kind 
 
-and occurence_args k kind args = 
-  Array.fold_left (occurence k) kind args
+and occurrence_args k kind args =
+  Array.fold_left (occurrence k) kind args
     
 let occur_once lam = 
-  try let _ = occurence 1 true lam in true
+  try let _ = occurrence 1 true lam in true
   with Not_found -> false
       
 (* [remove_let lam] remove let expression in [lam] if the variable is *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 29c6009ce4..6e1c3c5b72 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -733,14 +733,9 @@ let vm_conv cv_pb env t1 t2 =
     Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
     fconv cv_pb false (fun _->None) env t1 t2
 
-
-let default_conv = ref (fun cv_pb ?(l2r=false) -> fconv cv_pb l2r (fun _->None))
-
-let set_default_conv f = default_conv := f
-
 let default_conv cv_pb ?(l2r=false) env t1 t2 =
   try
-    !default_conv ~l2r cv_pb env t1 t2
+    fconv cv_pb false (fun _ -> None) env t1 t2
   with Not_found | Invalid_argument _ ->
     Pp.msg_warning (Pp.str "Compilation failed, falling back to standard conversion");
     fconv cv_pb false (fun _->None) env t1 t2
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index a22f3730e9..2c1c0ec051 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -93,7 +93,6 @@ val set_nat_conv :
   (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit
 val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function
 
-val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit
 val default_conv     : conv_pb -> ?l2r:bool -> types conversion_function
 val default_conv_leq : ?l2r:bool -> types conversion_function
 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 8af2efc588..27e184ea3f 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -40,8 +40,6 @@ let conv_vect fconv vect1 vect2 cu =
     !rcu
   else raise NotConvertible
 
-let infos = ref (create_clos_infos betaiotazeta Environ.empty_env)
-
 let rec conv_val env pb k v1 v2 cu =
   if v1 == v2 then cu
   else conv_whd env pb k (whd_val v1) (whd_val v2) cu
@@ -219,7 +217,6 @@ and conv_eq_vect env vt1 vt2 cu =
   else raise NotConvertible
 
 let vconv pb env t1 t2 =
-  infos := create_clos_infos betaiotazeta env;
   let _cu =
     try conv_eq env pb t1 t2 (universes env)
     with NotConvertible ->
@@ -230,14 +227,3 @@ let vconv pb env t1 t2 =
   in ()
 
 let _ = Reduction.set_vm_conv vconv
-
-let use_vm = ref false
-
-let set_use_vm b =
-  use_vm := b;
-  if b then Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> vconv cv_pb)
-  else Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> Reduction.conv_cmp cv_pb)
-
-let use_vm _ = !use_vm
-
-
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 096d31ac81..1a29a4d518 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -12,8 +12,6 @@ open Reduction
 
 (**********************************************************************
   s conversion functions *)
-val use_vm : unit -> bool
-val set_use_vm : bool -> unit
 val vconv : conv_pb -> types conversion_function
 
 val val_of_constr : env -> constr -> values