Merge v8.5 into trunk

Conflicts:
	tactics/eauto.ml4

(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)

5 files changed, 18 insertions, 8 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 2c9c695bfd..a2cccc0e0b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -28,7 +28,7 @@ open Misctypes
 (* Abbreviations *)
 
 let pf_env = Refiner.pf_env
-let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
+let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma c
 
 (******************************************************************)
 (* Clausal environments *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 898588d9e4..5c48995fc7 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -83,7 +83,7 @@ let apply_to_hyp sign id f =
     else sign
 
 let check_typability env sigma c =
-  if !check then let _ = type_of env sigma c in ()
+  if !check then let _ = unsafe_type_of env sigma c in ()
 
 (************************************************************************)
 (************************************************************************)
@@ -317,7 +317,7 @@ let meta_free_prefix a =
   with Stop acc -> Array.rev_of_list acc
 
 let goal_type_of env sigma c =
-  if !check then type_of env sigma c
+  if !check then unsafe_type_of env sigma c
   else Retyping.get_type_of env sigma c
 
 let rec mk_refgoals sigma goal goalacc conclty trm =
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index d25f7e9150..f172bbdd1a 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -30,9 +30,13 @@ let cbv_vm env sigma c =
   Vnorm.cbv_vm env c ctyp
 
 let cbv_native env sigma c =
-  let ctyp = Retyping.get_type_of env sigma c in
-  let evars = Nativenorm.evars_of_evar_map sigma in
-  Nativenorm.native_norm env evars c ctyp
+  if Coq_config.no_native_compiler then
+    let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in
+    cbv_vm env sigma c
+  else
+    let ctyp = Retyping.get_type_of env sigma c in
+    let evars = Nativenorm.evars_of_evar_map sigma in
+    Nativenorm.native_norm env evars c ctyp
 
 let whd_cbn flags env sigma t =
   let (state,_) =
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index fa0d03623c..4238d1e372 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -84,6 +84,7 @@ let pf_nf                        = pf_reduce simpl
 let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
+let pf_unsafe_type_of            = pf_reduce unsafe_type_of
 let pf_type_of                   = pf_reduce type_of
 let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
@@ -172,6 +173,9 @@ module New = struct
   let pf_env = Proofview.Goal.env
   let pf_concl = Proofview.Goal.concl
 
+  let pf_unsafe_type_of gl t =
+    pf_apply unsafe_type_of gl t
+
   let pf_type_of gl t =
     pf_apply type_of gl t
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f7fc6b54f1..a0e1a01577 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -41,7 +41,8 @@ val pf_nth_hyp_id         : goal sigma -> int -> Id.t
 val pf_last_hyp           : goal sigma -> named_declaration
 val pf_ids_of_hyps        : goal sigma -> Id.t list
 val pf_global             : goal sigma -> Id.t -> constr
-val pf_type_of            : goal sigma -> constr -> types
+val pf_unsafe_type_of            : goal sigma -> constr -> types
+val pf_type_of            : goal sigma -> constr -> evar_map * types
 val pf_hnf_type_of        : goal sigma -> constr -> types
 
 val pf_get_hyp            : goal sigma -> Id.t -> named_declaration
@@ -112,7 +113,8 @@ module New : sig
   val pf_env : 'a Proofview.Goal.t -> Environ.env
   val pf_concl : [ `NF ] Proofview.Goal.t -> types
 
-  val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types
   val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool
 
   val pf_get_new_id  : identifier -> [ `NF ] Proofview.Goal.t -> identifier