From eef0ffe1646d09c81de23ad34f58a75d63a88372 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 10 May 2015 19:41:12 +0200
Subject: Code factorization in Constr_matching.

---
 pretyping/constr_matching.ml | 52 +++++++++++++++++---------------------------
 1 file changed, 20 insertions(+), 32 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index e281807131..5098665582 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
+      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 =
-- 
cgit v1.2.3


From a49cd60c67aca452500c82aad61327823f9abe31 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2015 14:16:19 +0200
Subject: Fixing bug #4234.

---
 pretyping/evarutil.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2508f4ef3b..6d076ecd11 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 =
-- 
cgit v1.2.3


From 574b4096517b4ac9189c2226e1cd75745e788db0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 May 2015 09:11:22 +0200
Subject: Better fixing #4198 such that the term to match is looked for before
 the predicate, thus respecting the visual left-to-right top-down order (see
 a45bd5981092).

This fixes CFGV.
---
 pretyping/constr_matching.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 5098665582..a0493777a5 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -419,7 +419,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
       | [] -> 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 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
-- 
cgit v1.2.3


From f86b7d3b8cb23e2fc19a936accb421bfdbf2cb4d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2015 12:54:07 +0200
Subject: Fix for a second avatar of bug #4234.

---
 pretyping/evarutil.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6d076ecd11..ee6bbe7fbe 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -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... *)
-- 
cgit v1.2.3


From 3a7095f9f6a09a4461c2124b0020dfe37962de26 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2015 17:47:24 +0200
Subject: Safer typing primitives.

Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.

- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.

All uses of unsafe_* functions should be eventually eliminated.
---
 pretyping/cases.ml       |  6 +++---
 pretyping/coercion.ml    |  8 ++++----
 pretyping/pretyping.ml   |  2 +-
 pretyping/tacred.ml      |  2 +-
 pretyping/typing.ml      | 13 +++++++++++--
 pretyping/typing.mli     |  9 ++++++---
 pretyping/unification.ml |  4 ++--
 7 files changed, 28 insertions(+), 16 deletions(-)

(limited to 'pretyping')

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/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
-- 
cgit v1.2.3


From 4ad6855504db2ce15a474bd646e19151aa8142e2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 14 May 2015 09:53:36 +0200
Subject: Disable precompilation for native_compute by default.

Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.

Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.

If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.

Failure to precompile is a hard error, since it is now explicitly required
by the user.
---
 pretyping/nativenorm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

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 
   (*
-- 
cgit v1.2.3