Merge branch 'v8.5' into trunk

1 files changed, 6 insertions, 26 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 6e1c3c5b7..e081870ba 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -26,8 +26,6 @@ open Environ
 open Closure
 open Esubst
 
-let left2right = ref false
-
 let rec is_empty_stack = function
   [] -> true
   | Zupdate _::s -> is_empty_stack s
@@ -208,9 +206,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
           let cu1 = cmp_rec s1 s2 cuniv in
           (match (z1,z2) with
             | (Zlapp a1,Zlapp a2) -> 
-	      if !left2right then
-		Array.fold_left2 (fun cu x y -> f x y cu) cu1 a1 a2
-	      else Array.fold_right2 f a1 a2 cu1
+	       Array.fold_right2 f a1 a2 cu1
 	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
 	      if not (eq_constant c1 c2) then 
 		raise NotConvertible
@@ -632,7 +628,7 @@ let infer_cmp_universes env pb s0 s1 univs =
 let infer_convert_instances flex u u' (univs,cstrs) =
   (univs, Univ.enforce_eq_instances u u' cstrs)
 
-let infered_universes : (UGraph.t * Univ.Constraint.t) universe_compare = 
+let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = 
   { compare = infer_cmp_universes;
     compare_instances = infer_convert_instances }
 
@@ -665,7 +661,7 @@ let trans_conv_universes ?(l2r=false) ?(evars=fun _->None) reds =
 let trans_conv_leq_universes ?(l2r=false) ?(evars=fun _->None) reds = 
   trans_fconv_universes reds CUMUL l2r evars
 
-let fconv = trans_fconv (Id.Pred.full, Cpred.full)
+let fconv = trans_fconv full_transparent_state
 
 let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None)
 let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars
@@ -680,7 +676,7 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
     v1
     v2
 
-let generic_conv cv_pb l2r evars reds env univs t1 t2 =
+let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
   let (s, _) = 
     clos_fconv reds cv_pb l2r evars env univs t1 t2 
   in s
@@ -692,7 +688,7 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
   in
     if b then cstrs
     else
-      let univs = ((univs, Univ.Constraint.empty), infered_universes) in
+      let univs = ((univs, Univ.Constraint.empty), inferred_universes) in
       let ((_,cstrs), _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in
 	cstrs
 
@@ -711,19 +707,7 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta
     env univs t1 t2 = 
   infer_conv_universes CUMUL l2r evars ts env univs t1 t2
 
-(* option for conversion *)
-let nat_conv = ref (fun cv_pb sigma ->
-		    fconv cv_pb false (sigma.Nativelambda.evars_val))
-let set_nat_conv f = nat_conv := f
-
-let native_conv cv_pb sigma env t1 t2 =
-  if eq_constr t1 t2 then ()
-  else begin
-    let t1 = (it_mkLambda_or_LetIn t1 (rel_context env)) in
-    let t2 = (it_mkLambda_or_LetIn t2 (rel_context env)) in
-    !nat_conv cv_pb sigma env t1 t2 
-  end
-
+(* This reference avoids always having to link C code with the kernel *)
 let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
 let set_vm_conv f = vm_conv := f
 let vm_conv cv_pb env t1 t2 =
@@ -734,11 +718,7 @@ let vm_conv cv_pb env t1 t2 =
     fconv cv_pb false (fun _->None) env t1 t2
 
 let default_conv cv_pb ?(l2r=false) env t1 t2 =
-  try
     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
 
 let default_conv_leq = default_conv CUMUL
 (*