Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

1 files changed, 13 insertions, 27 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index ea9b2755f2..bf3801e547 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -245,10 +245,12 @@ and 'a infos = {
 let info_flags info = info.i_flags
 let info_env info = info.i_cache.i_env
 
+open Context.Named.Declaration
+
 let rec assoc_defined id = function
 | [] -> raise Not_found
-| (_, None, _) :: ctxt -> assoc_defined id ctxt
-| (id', Some c, _) :: ctxt ->
+| LocalAssum _ :: ctxt -> assoc_defined id ctxt
+| LocalDef (id', c, _) :: ctxt ->
   if Id.equal id id' then c else assoc_defined id ctxt
 
 let ref_value_cache ({i_cache = cache} as infos)  ref =
@@ -285,9 +287,10 @@ let defined_rels flags env =
   let ctx = rel_context env in
   let len = List.length ctx in
   let ans = Array.make len None in
-  let iter i (_, b, _) = match b with
-  | None -> ()
-  | Some _ -> Array.unsafe_set ans i b
+  let open Context.Rel.Declaration in
+  let iter i = function
+    | LocalAssum _ -> ()
+    | LocalDef (_,b,_) -> Array.unsafe_set ans i (Some b)
   in
   let () = List.iteri iter ctx in
   ans
@@ -346,7 +349,6 @@ and fterm =
   | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
-  | FCase of case_info * fconstr * fconstr * fconstr array
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
   | FLambda of int * (Name.t * constr) list * constr * fconstr subs
   | FProd of Name.t * fconstr * fconstr
@@ -376,7 +378,6 @@ let update v1 no t =
 
 type stack_member =
   | Zapp of fconstr array
-  | Zcase of case_info * fconstr * fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
   | Zproj of int * int * constant
   | Zfix of fconstr * stack
@@ -569,10 +570,6 @@ let rec to_constr constr_fun lfts v =
     | FFlex (ConstKey op) -> mkConstU op
     | FInd op -> mkIndU op
     | FConstruct op -> mkConstructU op
-    | FCase (ci,p,c,ve) ->
-	mkCase (ci, constr_fun lfts p,
-                constr_fun lfts c,
-		CArray.Fun1.map constr_fun lfts ve)
     | FCaseT (ci,p,c,ve,env) ->
 	mkCase (ci, constr_fun lfts (mk_clos env p),
                 constr_fun lfts c,
@@ -646,9 +643,6 @@ let rec zip m stk =
   match stk with
     | [] -> m
     | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s
-    | Zcase(ci,p,br)::s ->
-        let t = FCase(ci, p, m, br) in
-        zip {norm=neutr m.norm; term=t} s
     | ZcaseT(ci,p,br,e)::s ->
         let t = FCaseT(ci, p, m, br, e) in
         zip {norm=neutr m.norm; term=t} s
@@ -731,7 +725,7 @@ let rec get_args n tys f e stk =
 
 (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
 let rec eta_expand_stack = function
-  | (Zapp _ | Zfix _ | Zcase _ | ZcaseT _ | Zproj _ 
+  | (Zapp _ | Zfix _ | ZcaseT _ | Zproj _
 	| Zshift _ | Zupdate _ as e) :: s ->
       e :: eta_expand_stack s
   | [] ->
@@ -771,7 +765,7 @@ let drop_parameters depth n argstk =
   (* we know that n < stack_args_size(argstk) (if well-typed term) *) 
   anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor")
 
-(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding 
+(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding
     to the conversion of the eta expansion of t, considered as an inhabitant 
     of ind, and the Constructor c of this inductive type applied to arguments
     s.
@@ -784,7 +778,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (Some (_,projs,pbs)) when
-	mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
+	mib.Declarations.mind_finite == Decl_kinds.BiFinite -> 
 	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.Declarations.mind_nparams in
@@ -842,7 +836,6 @@ let rec knh info m stk =
     | FCLOS(t,e) -> knht info e t (zupdate m stk)
     | FLOCKED -> assert false
     | FApp(a,b) -> knh info a (append_stack b (zupdate m stk))
-    | FCase(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk)
     | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate m stk)
     | FFix(((ri,n),(_,_,_)),_) ->
         (match get_nth_arg m ri.(n) stk with
@@ -904,10 +897,6 @@ let rec knr info m stk =
         | None -> (set_norm m; (m,stk)))
   | FConstruct((ind,c),u) when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
-          (depth, args, Zcase(ci,_,br)::s) ->
-            assert (ci.ci_npar>=0);
-            let rargs = drop_parameters depth ci.ci_npar args in
-            kni info br.(c-1) (rargs@s)
         | (depth, args, ZcaseT(ci,_,br,e)::s) ->
             assert (ci.ci_npar>=0);
             let rargs = drop_parameters depth ci.ci_npar args in
@@ -924,7 +913,7 @@ let rec knr info m stk =
         | (_,args,s) -> (m,args@s))
   | FCoFix _ when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
-          (_, args, (((Zcase _|ZcaseT _|Zproj _)::_) as stk')) ->
+          (_, args, (((ZcaseT _|Zproj _)::_) as stk')) ->
             let (fxe,fxbd) = contract_fix_vect m.term in
             knit info fxe fxbd (args@stk')
         | (_,args,s) -> (m,args@s))
@@ -953,9 +942,6 @@ let rec zip_term zfun m stk =
     | [] -> m
     | Zapp args :: s ->
         zip_term zfun (mkApp(m, Array.map zfun args)) s
-    | Zcase(ci,p,br)::s ->
-        let t = mkCase(ci, zfun p, m, Array.map zfun br) in
-        zip_term zfun t s
     | ZcaseT(ci,p,br,e)::s ->
         let t = mkCase(ci, zfun (mk_clos e p), m,
 		       Array.map (fun b -> zfun (mk_clos e b)) br) in