From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Wed, 15 Jul 2015 10:36:12 +0200
Subject: Imported Upstream version 8.5~beta2+dfsg

---
 pretyping/reductionops.ml | 52 ++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 40 insertions(+), 12 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a23963ab..dd671f11 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -60,13 +60,20 @@ module ReductionBehaviour = struct
 
   let discharge = function
     | _,(ReqGlobal (ConstRef c, req), (_, b)) ->
-       let c' = pop_con c in
-       let vars, _subst, _ctx = Lib.section_segment_of_constant c in
-       let extra = List.length vars in
-       let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in
-       let recargs' = List.map ((+) extra) b.b_recargs in
-       let b' = { b with b_nargs = nargs'; b_recargs = recargs' } in
-       Some (ReqGlobal (ConstRef c', req), (ConstRef c', b'))
+      let b =
+        if Lib.is_in_section (ConstRef c) then
+          let vars, _, _ = Lib.section_segment_of_constant c in
+          let extra = List.length vars in
+          let nargs' =
+             if b.b_nargs = max_int then max_int
+             else if b.b_nargs < 0 then b.b_nargs
+             else b.b_nargs + extra in
+          let recargs' = List.map ((+) extra) b.b_recargs in
+          { b with b_nargs = nargs'; b_recargs = recargs' }
+        else b
+      in
+      let c = Lib.discharge_con c in
+      Some (ReqGlobal (ConstRef c, req), (ConstRef c, b))
     | _ -> None
 
   let rebuild = function
@@ -842,7 +849,14 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 		    let (tm',sk'),cst_l' =
 		      whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
 		    in
-		      if equal_stacks (x, app_sk) (tm', sk') || Stack.will_expose_iota sk'
+		    let rec is_case x = match kind_of_term x with
+		      | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
+		      | App (hd, _) -> is_case hd
+		      | Case _ -> true
+		      | _ -> false in
+		    if equal_stacks (x, app_sk) (tm', sk')
+		       || Stack.will_expose_iota sk'
+		       || is_case tm'
 		      then fold ()
 		      else whrec cst_l' (tm', sk' @ sk)
 		  else match recargs with
@@ -980,7 +994,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
     | CoFix cofix ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
-	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	|args, ((Stack.Case _ |Stack.Proj _)::s') ->
 	  reduce_and_refold_cofix whrec env cst_l cofix stack
 	|_ -> fold ()
       else fold ()
@@ -1059,7 +1073,7 @@ let local_whd_state_gen flags sigma =
     | CoFix cofix ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
-	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	|args, ((Stack.Case _ | Stack.Proj _)::s') ->
 	  whrec (contract_cofix cofix, stack)
 	|_ -> s
       else s
@@ -1279,7 +1293,8 @@ let sigma_univ_state =
   { Reduction.compare = sigma_compare_sorts;
     Reduction.compare_instances = sigma_compare_instances }
 
-let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = 
+let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) 
+    env sigma x y = 
   try 
     let b, sigma = 
       let b, cstrs = 
@@ -1301,7 +1316,7 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
 	  sigma', true
   with
   | Reduction.NotConvertible -> sigma, false
-  | Univ.UniverseInconsistency _ -> sigma, false
+  | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
   | e when is_anomaly e -> error "Conversion test raised an anomaly"
     
 (********************************************************************)
@@ -1617,3 +1632,16 @@ let head_unfold_under_prod ts env _ c =
 	    | Const cst -> beta_applist (unfold cst,l)
 	    | _ -> c in
   aux c
+
+let betazetaevar_applist sigma n c l =
+  let rec stacklam n env t stack =
+    if Int.equal n 0 then applist (substl env t, stack) else
+    match kind_of_term t, stack with
+    | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
+    | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
+    | Evar ev, _ ->
+      (match safe_evar_value sigma ev with
+      | Some body -> stacklam n env body stack
+      | None -> applist (substl env t, stack))
+    | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+  stacklam n [] c l
-- 
cgit v1.2.3