Merge v8.5 into trunk

Conflicts:
	tactics/eauto.ml4

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

10 files changed, 55 insertions, 53 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fcbe90b6a7..ef196e0a72 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1668,7 +1668,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
 	(lift (n'-n) impossible_case_type, mkSort u)
     | Some t ->
         let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
-        let evd,tt = Typing.e_type_of extenv !evdref t in
+        let evd,tt = Typing.type_of extenv !evdref t in
         evdref := evd;
         (t,tt) in
   let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
@@ -2014,7 +2014,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	let IndType (indf, _) = 
 	  try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty)
 	  with Not_found -> error_case_not_inductive env 
-	    {uj_val = ty; uj_type = Typing.type_of env !evdref ty}
+	    {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty}
 	in
 	let (ind,u), params = dest_ind_family indf in
 	if not (eq_ind ind cind) then error_bad_constructor_loc l env cstr ind;
@@ -2214,7 +2214,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	 let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
-	 let _btype = evd_comb1 (Typing.e_type_of env) evdref bbody in
+	 let _btype = evd_comb1 (Typing.type_of env) evdref bbody in
 	 let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
 	 let branch =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 8ebb8cd27b..f5135f5c60 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -295,8 +295,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		   let evm = !evdref in
 		     (try subco ()
 		      with NoSubtacCoercion ->
-			let typ = Typing.type_of env evm c in
-			let typ' = Typing.type_of env evm c' in
+			let typ = Typing.unsafe_type_of env evm c in
+			let typ' = Typing.unsafe_type_of env evm c' in
 			  (* 			     if not (is_arity env evm typ) then *)
 			  coerce_application typ typ' c c' l l')
 		       (* 			     else subco () *)
@@ -305,8 +305,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 	   | x, y when Constr.equal c c' ->
 	       if Int.equal (Array.length l) (Array.length l') then
 		 let evm =  !evdref in
-		 let lam_type = Typing.type_of env evm c in
-		 let lam_type' = Typing.type_of env evm c' in
+		 let lam_type = Typing.unsafe_type_of env evm c in
+		 let lam_type' = Typing.unsafe_type_of env evm c' in
 		   (* 			 if not (is_arity env evm lam_type) then ( *)
 		   coerce_application lam_type lam_type' c c' l l'
 		     (* 			 ) else subco () *)
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index e281807131..a0493777a5 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -343,56 +343,49 @@ let matches_head env sigma pat c =
   matches env sigma pat head
 
 (* Tells if it is an authorized occurrence and if the instance is closed *)
-let authorized_occ env sigma partial_app closed pat c mk_ctx next =
+let authorized_occ env sigma partial_app closed pat c mk_ctx =
   try
     let subst = matches_core_closed env sigma false partial_app pat c in
     if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd subst)
-    then next ()
-    else mkresult subst (mk_ctx (mkMeta special_meta)) next
-  with PatternMatchingFailure -> next ()
+    then (fun next -> next ())
+    else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next)
+  with PatternMatchingFailure -> (fun next -> next ())
 
 let subargs env v = Array.map_to_list (fun c -> (env, c)) v
 
 (* Tries to match a subterm of [c] with [pat] *)
 let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
   let rec aux env c mk_ctx next =
-  match kind_of_term c with
+  let here = authorized_occ env sigma partial_app closed pat c mk_ctx in
+  let next () = match kind_of_term c with
   | Cast (c1,k,c2) ->
       let next_mk_ctx = function
       | [c1] -> mk_ctx (mkCast (c1, k, c2))
       | _ -> assert false
       in
-      let next () = try_aux [env, c1] next_mk_ctx next in
-      authorized_occ env sigma partial_app closed pat c mk_ctx next
+      try_aux [env, c1] next_mk_ctx next
   | Lambda (x,c1,c2) ->
       let next_mk_ctx = function
       | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2))
       | _ -> assert false
       in
-      let next () = 
-	let env' = Environ.push_rel (x,None,c1) env in
-        try_aux [(env, c1); (env', c2)] next_mk_ctx next in
-      authorized_occ env sigma partial_app closed pat c mk_ctx next
+      let env' = Environ.push_rel (x,None,c1) env in
+      try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | Prod (x,c1,c2) ->
       let next_mk_ctx = function
       | [c1; c2] -> mk_ctx (mkProd (x, c1, c2))
       | _ -> assert false
       in
-      let next () = 
-	let env' = Environ.push_rel (x,None,c1) env in
-        try_aux [(env, c1); (env', c2)] next_mk_ctx next in
-      authorized_occ env sigma partial_app closed pat c mk_ctx next
+      let env' = Environ.push_rel (x,None,c1) env in
+      try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | LetIn (x,c1,t,c2) ->
       let next_mk_ctx = function
       | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2))
       | _ -> assert false
       in
-      let next () = 
-	let env' = Environ.push_rel (x,Some c1,t) env in
-        try_aux [(env, c1); (env', c2)] next_mk_ctx next in
-      authorized_occ env sigma partial_app closed pat c mk_ctx next
+      let env' = Environ.push_rel (x,Some c1,t) env in
+      try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | App (c1,lc) ->
-      let next () =
         let topdown = true in
         if partial_app then
           if topdown then
@@ -421,45 +414,40 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
             mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
           let sub = (env, c1) :: subargs env lc in
           try_aux sub mk_ctx next
-      in
-      authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Case (ci,hd,c1,lc) ->
       let next_mk_ctx = function
       | [] -> assert false
       | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
       in
-      let sub = (env, hd) :: (env, c1) :: subargs env lc in
-      let next () = try_aux sub next_mk_ctx next in
-      authorized_occ env sigma partial_app closed pat c mk_ctx next
+      let sub = (env, c1) :: (env, hd) :: subargs env lc in
+      try_aux sub next_mk_ctx next
   | Fix (indx,(names,types,bodies)) ->
     let nb_fix = Array.length types in
     let next_mk_ctx le =
       let (ntypes,nbodies) = CList.chop nb_fix le in
       mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in
     let sub = subargs env types @ subargs env bodies in
-    let next () = try_aux sub next_mk_ctx next in
-    authorized_occ env sigma partial_app closed pat c mk_ctx next
+    try_aux sub next_mk_ctx next
   | CoFix (i,(names,types,bodies)) ->
     let nb_fix = Array.length types in
     let next_mk_ctx le =
       let (ntypes,nbodies) = CList.chop nb_fix le in
       mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in
     let sub = subargs env types @ subargs env bodies in
-    let next () = try_aux sub next_mk_ctx next in
-    authorized_occ env sigma partial_app closed pat c mk_ctx next
+    try_aux sub next_mk_ctx next
   | Proj (p,c') ->
     let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
-    let next () = 
       if partial_app then
 	try 
 	  let term = Retyping.expand_projection env sigma p c' [] in
 	    aux env term mk_ctx next
 	with Retyping.RetypeError _ -> next ()
       else
-      try_aux [env, c'] next_mk_ctx next in
-      authorized_occ env sigma partial_app closed pat c mk_ctx next
+      try_aux [env, c'] next_mk_ctx next
   | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
-      authorized_occ env sigma partial_app closed pat c mk_ctx next
+    next ()
+  in
+  here next
 
   (* Tries [sub_match] for all terms in the list *)
   and try_aux lc mk_ctx next =
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2508f4ef3b..ee6bbe7fbe 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -713,7 +713,7 @@ let define_pure_evar_as_product evd evk =
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
   let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
-  let concl = whd_evar evd evi.evar_concl in
+  let concl = whd_betadeltaiota evenv evd evi.evar_concl in
   let s = destSort concl in
   let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
   let evd2,rng =
@@ -795,8 +795,10 @@ let define_evar_as_sort env evd (ev,args) =
   let evd, u = new_univ_variable univ_rigid evd in
   let evi = Evd.find_undefined evd ev in 
   let s = Type u in
+  let concl = whd_betadeltaiota (evar_env evi) evd evi.evar_concl in
+  let sort = destSort concl in
   let evd' = Evd.define ev (mkSort s) evd in
-    Evd.set_leq_sort env evd' (Type (Univ.super u)) (destSort evi.evar_concl), s
+  Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
 
 (* We don't try to guess in which sort the type should be defined, since
    any type has type Type. May cause some trouble, but not so far... *)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index bd427ecd08..ac4e3b3064 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -378,8 +378,8 @@ and  nf_predicate env ind mip params v pT =
   | _, _ -> false, nf_type env v
 
 let native_norm env sigma c ty =  
-  if !Flags.no_native_compiler then
-    error "Native_compute reduction has been disabled"
+  if Coq_config.no_native_compiler then
+    error "Native_compute reduction has been disabled at configure time."
   else
   let penv = Environ.pre_env env in 
   (*
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0cadffa4fe..03fe2122c0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -374,7 +374,7 @@ let pretype_ref loc evdref env ref us =
   | ref ->
     let evd, c = pretype_global loc univ_flexible env !evdref ref us in
     let () = evdref := evd in
-    let ty = Typing.type_of env evd c in
+    let ty = Typing.unsafe_type_of env evd c in
       make_judge c ty
 
 let judge_of_Type evd s =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 372b26aa25..8a5db90590 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1134,7 +1134,7 @@ let abstract_scheme env (locc,a) (c, sigma) =
 let pattern_occs loccs_trm env sigma c =
   let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (c,sigma) in
   try
-    let _ = Typing.type_of env sigma abstr_trm in
+    let _ = Typing.unsafe_type_of env sigma abstr_trm in
       sigma, applist(abstr_trm, List.map snd loccs_trm)
   with Type_errors.TypeError (env',t) ->
     raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c6209cc33a..fb5927dbf7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -270,7 +270,7 @@ let check env evdref c t =
 
 (* Type of a constr *)
 
-let type_of env evd c =
+let unsafe_type_of env evd c =
   let j = execute env (ref evd) c in
     j.uj_type
 
@@ -283,7 +283,7 @@ let sort_of env evdref c =
 
 (* Try to solve the existential variables by typing *)
 
-let e_type_of ?(refresh=false) env evd c =
+let type_of ?(refresh=false) env evd c =
   let evdref = ref evd in
   let j = execute env evdref c in
   (* side-effect on evdref *)
@@ -291,6 +291,15 @@ let e_type_of ?(refresh=false) env evd c =
       Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type
     else !evdref, j.uj_type
 
+let e_type_of ?(refresh=false) env evdref c =
+  let j = execute env evdref c in
+  (* side-effect on evdref *)
+    if refresh then
+      let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in
+      let () = evdref := evd in
+      c
+    else j.uj_type
+
 let solve_evars env evdref c =
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1f822f1a58..bfae46ff80 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -13,12 +13,15 @@ open Evd
 (** This module provides the typing machine with existential variables
     and universes. *)
 
-(** Typecheck a term and return its type *)
-val type_of : env -> evar_map -> constr -> types
+(** Typecheck a term and return its type. May trigger an evarmap leak. *)
+val unsafe_type_of : env -> evar_map -> constr -> types
 
 (** Typecheck a term and return its type + updated evars, optionally refreshing
     universes *)
-val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
+val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
+
+(** Variant of [type_of] using references instead of state-passing. *)
+val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
 
 (** Typecheck a type and return its sort *)
 val sort_of : env -> evar_map ref -> types -> sorts
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c2281e13a5..b5fe5d0b6d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -93,7 +93,7 @@ let abstract_list_all env evd typ c l =
   let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in
   let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in
   let evd,typp =
-    try Typing.e_type_of env evd p
+    try Typing.type_of env evd p
     with
     | UserError _ ->
         error_cannot_find_well_typed_abstraction env evd p l None
@@ -1150,7 +1150,7 @@ let applyHead env evd n c  =
 	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
       | _ -> error "Apply_Head_Then"
   in
-    apprec n c (Typing.type_of env evd c) evd
+    apprec n c (Typing.unsafe_type_of env evd c) evd
     
 let is_mimick_head ts f =
   match kind_of_term f with