Imported Upstream version 8.3pl1upstream/8.3pl1

14 files changed, 192 insertions, 167 deletions

diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 34b32c0a..ceadd26e 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -719,7 +719,7 @@ and tr_formula tv bv env f =
     | _, [a;b] when c = Lazy.force coq_iff ->
 	Iff (tr_formula tv bv env a, tr_formula tv bv env b)
     | Prod (n, a, b), _ ->
-	if is_imp_term f then
+        if is_Prop (Typing.type_of env Evd.empty a) then
 	  Imp (tr_formula tv bv env a, tr_formula tv bv env b)
 	else
 	  let id, t, bv, env, b = quantifiers n a b tv bv env in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index b615955f..5329c675 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraction.ml 13427 2010-09-17 17:37:52Z letouzey $ i*)
+(*i $Id: extraction.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
 
 (*i*)
 open Util
@@ -29,7 +29,7 @@ open Table
 open Mlutil
 (*i*)
 
-exception I of inductive_info
+exception I of inductive_kind
 
 (* A set of all fixpoint functions currently being extracted *)
 let current_fixpoints = ref ([] : constant list)
@@ -368,7 +368,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     in
 
     add_ind kn mib
-      {ind_info = Standard;
+      {ind_kind = Standard;
        ind_nparams = npar;
        ind_packets = packets;
        ind_equiv = equiv
@@ -453,7 +453,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	Record field_glob
       with (I info) -> info
     in
-    let i = {ind_info = ind_info;
+    let i = {ind_kind = ind_info;
 	     ind_nparams = npar;
 	     ind_packets = packets;
 	     ind_equiv = equiv }
@@ -711,9 +711,15 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
   let magic2 = needs_magic (a, mlt) in
   let head mla =
-    if mi.ind_info = Singleton then
+    if mi.ind_kind = Singleton then
       put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
-    else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla))
+    else
+      let typeargs = match snd (type_decomp type_cons) with
+	| Tglob (_,l) -> List.map type_simpl l
+	| _ -> assert false
+      in
+      let info = {c_kind = mi.ind_kind; c_typs = typeargs} in
+      put_magic_if magic1 (MLcons (info, ConstructRef cp, mla))
   in
   (* Different situations depending of the number of arguments: *)
   if la < params_nb then
@@ -779,7 +785,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in
 	(r, List.rev ids, e')
       in
-      if mi.ind_info = Singleton then
+      if mi.ind_kind = Singleton then
 	begin
 	  (* Informative singleton case: *)
 	  (* [match c with C i -> t] becomes [let i = c' in t'] *)
@@ -790,7 +796,9 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	end
       else
 	(* Standard case: we apply [extract_branch]. *)
-	MLcase ((mi.ind_info,BranchNone), a, Array.init br_size extract_branch)
+	let typs = List.map type_simpl (Array.to_list metas) in
+	let info = { m_kind = mi.ind_kind; m_typs = typs; m_same = BranchNone }
+	in MLcase (info, a, Array.init br_size extract_branch)
 
 (*s Extraction of a (co)-fixpoint. *)
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 29d3da4d..1c47ad81 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: haskell.ml 13414 2010-09-14 13:28:15Z glondu $ i*)
+(*i $Id: haskell.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
 
 (*s Production of Haskell syntax. *)
 
@@ -156,10 +156,10 @@ let rec pp_expr par env args =
 	hov 2 (str (find_custom_match pv) ++ fnl () ++
 		 prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv
 	       ++ pp_expr true env [] t)
-    | MLcase ((_,factors),t, pv) ->
+    | MLcase (info,t, pv) ->
       	apply (pp_par par'
 		 (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
-		       fnl () ++ str "  " ++ pp_pat env factors pv)))
+		       fnl () ++ str "  " ++ pp_pat env info pv)))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
@@ -172,7 +172,7 @@ let rec pp_expr par env args =
 	pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
     | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
 
-and pp_pat env factors pv =
+and pp_pat env info pv =
   let pp_one_pat (name,ids,t) =
     let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
     let par = expr_needs_par t in
@@ -184,27 +184,32 @@ and pp_pat env factors pv =
 			 (fun () -> (spc ())) pr_id (List.rev ids))) ++
 	   str " ->" ++ spc () ++ pp_expr par env' [] t)
   in
-  let factor_br, factor_l = try match factors with
-    | BranchFun (i::_ as l) -> check_function_branch pv.(i), l
-    | BranchCst (i::_ as l) -> ast_pop (check_constant_branch pv.(i)), l
-    | _ -> MLdummy, []
-  with Impossible -> MLdummy, []
+  let factor_br, factor_set = try match info.m_same with
+    | BranchFun ints ->
+        let i = Intset.choose ints in
+	branch_as_fun info.m_typs pv.(i), ints
+    | BranchCst ints ->
+        let i = Intset.choose ints in
+        ast_pop (branch_as_cst pv.(i)), ints
+    | BranchNone -> MLdummy, Intset.empty
+  with _ -> MLdummy, Intset.empty
   in
-  let par = expr_needs_par factor_br in
   let last = Array.length pv - 1 in
   prvecti
-    (fun i x -> if List.mem i factor_l then mt () else
+    (fun i x -> if Intset.mem i factor_set then mt () else
        (pp_one_pat pv.(i) ++
-       if i = last && factor_l = [] then mt () else
+       if i = last && Intset.is_empty factor_set then mt () else
        fnl () ++ str "  ")) pv
   ++
-  if factor_l = [] then mt () else match factors with
+  if Intset.is_empty factor_set then mt () else
+  let par = expr_needs_par factor_br in
+  match info.m_same with
     | BranchFun _ ->
-	let ids, env' = push_vars [anonymous_name] env in
-	pr_id (List.hd ids) ++ str " ->" ++ spc () ++
-	pp_expr par env' [] factor_br
+        let ids, env' = push_vars [anonymous_name] env in
+        pr_id (List.hd ids) ++ str " ->" ++ spc () ++
+	  pp_expr par env' [] factor_br
     | BranchCst _ ->
-	str "_ ->" ++ spc () ++ pp_expr par env [] factor_br
+        str "_ ->" ++ spc () ++ pp_expr par env [] factor_br
     | BranchNone -> mt ()
 
 (*s names of the functions ([ids]) are already pushed in [env],
@@ -286,7 +291,7 @@ let rec pp_ind first kn i ind =
 let pp_string_parameters ids = prlist (fun id -> str id ++ str " ")
 
 let pp_decl = function
-  | Dind (kn,i) when i.ind_info = Singleton ->
+  | Dind (kn,i) when i.ind_kind = Singleton ->
       pp_singleton (mind_of_kn kn) i.ind_packets.(0) ++ fnl ()
   | Dind (kn,i) -> hov 0 (pp_ind true (mind_of_kn kn) 0 i)
   | Dtype (r, l, t) ->
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 7ff11b90..20092815 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: miniml.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: miniml.mli 13733 2010-12-21 13:08:53Z letouzey $ i*)
 
 (*s Target language for extraction: a core ML called MiniML. *)
 
@@ -53,7 +53,7 @@ type ml_schema = int * ml_type
 
 (*s ML inductive types. *)
 
-type inductive_info =
+type inductive_kind =
   | Singleton
   | Coinductive
   | Standard
@@ -85,7 +85,7 @@ type equiv =
   | RenEquiv of string
 
 type ml_ind = {
-  ind_info : inductive_info;
+  ind_kind : inductive_kind;
   ind_nparams : int;
   ind_packets : ml_ind_packet array;
   ind_equiv : equiv
@@ -98,12 +98,27 @@ type ml_ident =
   | Id of identifier
   | Tmp of identifier
 
-(* list of branches to merge in a common pattern *)
+(** We now store some typing information on constructors
+    and cases to avoid type-unsafe optimisations.
+    For cases, we also store the set of branches to merge
+    in a common pattern, either "_ -> c" or "x -> f x"
+*)
+
+type constructor_info = {
+  c_kind : inductive_kind;
+  c_typs : ml_type list;
+}
 
-type case_info =
+type branch_same =
   | BranchNone
-  | BranchFun of int list
-  | BranchCst of int list
+  | BranchFun of Intset.t
+  | BranchCst of Intset.t
+
+type match_info = {
+  m_kind : inductive_kind;
+  m_typs : ml_type list;
+  m_same : branch_same
+}
 
 type ml_branch = global_reference * ml_ident list * ml_ast
 
@@ -113,8 +128,8 @@ and ml_ast =
   | MLlam    of ml_ident * ml_ast
   | MLletin  of ml_ident * ml_ast * ml_ast
   | MLglob   of global_reference
-  | MLcons   of inductive_info * global_reference * ml_ast list
-  | MLcase   of (inductive_info*case_info) * ml_ast * ml_branch array
+  | MLcons   of constructor_info * global_reference * ml_ast list
+  | MLcase   of match_info * ml_ast * ml_branch array
   | MLfix    of int * identifier array * ml_ast array
   | MLexn    of string
   | MLdummy
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index a079aacc..d467f508 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mlutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
+(*i $Id: mlutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
 
 (*i*)
 open Pp
@@ -291,6 +291,8 @@ let type_expand env t =
     | a -> a
   in if Table.type_expand () then expand t else t
 
+let type_simpl = type_expand (fun _ -> None)
+
 (*s Generating a signature from a ML type. *)
 
 let type_to_sign env t = match type_expand env t with
@@ -665,12 +667,23 @@ let rec ast_glob_subst s t = match t with
 
 (*S Auxiliary functions used in simplification of ML cases. *)
 
-(*s [check_function_branch (r,l,c)] checks if branch [c] can be seen
+(* Factorisation of some match branches into a common "x -> f x"
+   branch may break types sometimes. Example: [type 'x a = A].
+   Then [let id = function A -> A] has type ['x a -> 'y a],
+   which is incompatible with the type of [let id x = x].
+   We now check that the type arguments of the inductive are
+   preserved by our transformation.
+
+   TODO: this verification should be done someday modulo
+   expansion of type definitions.
+*)
+
+(*s [branch_as_function b typs (r,l,c)] tries to see branch [c]
   as a function [f] applied to [MLcons(r,l)]. For that it transforms
-  any [MLcons(r,l)] in [MLrel 1] and raises [Impossible] if any
-  variable in [l] occurs outside such a [MLcons] *)
+  any [MLcons(r,l)] in [MLrel 1] and raises [Impossible]
+  if any variable in [l] occurs outside such a [MLcons] *)
 
-let check_function_branch (r,l,c) =
+let branch_as_fun typs (r,l,c) =
   let nargs = List.length l in
   let rec genrec n = function
     | MLrel i as c ->
@@ -678,22 +691,32 @@ let check_function_branch (r,l,c) =
 	if i'<1 then c
 	else if i'>nargs then MLrel (i-nargs+1)
 	else raise Impossible
-    | MLcons(_,r',args) when r=r' && (test_eta_args_lift n nargs args) ->
+    | MLcons(i,r',args) when
+	r=r' && (test_eta_args_lift n nargs args) && typs = i.c_typs ->
 	MLrel (n+1)
     | a -> ast_map_lift genrec n a
   in genrec 0 c
 
-(*s [check_constant_branch (r,l,c)] checks if branch [c] is independent
-   from the pattern [MLcons(r,l)]. For that is raises [Impossible] if any
-   variable in [l] occurs in [c], and otherwise returns [c] lifted to
-   appear like a function with one arg (for uniformity with the
-   branch-as-function optimization) *)
+(*s [branch_as_cst (r,l,c)] tries to see branch [c] as a constant
+   independent from the pattern [MLcons(r,l)]. For that is raises [Impossible]
+   if any variable in [l] occurs in [c], and otherwise returns [c] lifted to
+   appear like a function with one arg (for uniformity with [branch_as_fun]).
+   NB: [MLcons(r,l)] might occur nonetheless in [c], but only when [l] is
+   empty, i.e. when [r] is a constant constructor
+*)
 
-let check_constant_branch (_,l,c) =
+let branch_as_cst (_,l,c) =
   let n = List.length l in
   if ast_occurs_itvl 1 n c then raise Impossible;
   ast_lift (1-n) c
 
+(* A branch [MLcons(r,l)->c] can be seen at the same time as a function
+   branch and a constant branch, either because:
+   - [MLcons(r,l)] doesn't occur in [c]. For example : "A -> B"
+   - this constructor is constant (i.e. [l] is empty). For example "A -> A"
+   When searching for the best factorisation below, we'll try both.
+*)
+
 (* The following structure allows to record which element occurred
    at what position, and then finally return the most frequent
    element and its positions. *)
@@ -702,61 +725,39 @@ let census_add, census_max, census_clean =
   let h = Hashtbl.create 13 in
   let clear () = Hashtbl.clear h in
   let add e i =
-    let l = try Hashtbl.find h e with Not_found -> [] in
-    Hashtbl.replace h e (i::l)
+    let s = try Hashtbl.find h e with Not_found -> Intset.empty in
+    Hashtbl.replace h e (Intset.add i s)
   in
   let max e0 =
-    let len = ref 0 and lst = ref [] and elm = ref e0 in
+    let len = ref 0 and lst = ref Intset.empty and elm = ref e0 in
     Hashtbl.iter
-      (fun e l ->
-	 let n = List.length l in
-	 if n > !len then begin len := n; lst := l; elm := e end)
+      (fun e s ->
+	 let n = Intset.cardinal s in
+	 if n > !len then begin len := n; lst := s; elm := e end)
       h;
     (!elm,!lst)
   in
   (add,max,clear)
 
-(* Given an abstraction function [abstr] (one of [check_*_branch]),
-   return the longest possible list of branches that have the
-   same abstraction, along with this abstraction. *)
+(* [factor_branches] return the longest possible list of branches
+   that have the same factorization, either as a function or as a
+   constant.
+*)
 
-let factor_branches abstr br =
+let factor_branches o typs br =
   census_clean ();
   for i = 0 to Array.length br - 1 do
-    try census_add (abstr br.(i)) i with Impossible -> ()
+    if o.opt_case_idr then
+      (try census_add (branch_as_fun typs br.(i)) i with Impossible -> ());
+    if o.opt_case_cst then
+      (try census_add (branch_as_cst br.(i)) i with Impossible -> ());
   done;
-  let br_factor, br_list = census_max MLdummy in
-  if br_list = [] then None
-  else if Array.length br >= 2 && List.length br_list < 2 then None
-  else Some (br_factor, br_list)
-
-(*s [check_generalizable_case] checks if all branches can be seen as the
-  same function [f] applied to the term matched. It is a generalized version
-  of both the identity case optimization and the constant case optimisation
-  ([f] can be a constant function) *)
-
-(* The optimisation [factor_branches check_function_branch] breaks types
-   in some special case. Example: [type 'x a = A].
-   Then [let f = function A -> A] has type ['x a -> 'y a],
-   which is incompatible with the type of [let f x = x].
-   We check first that there isn't such phantom variable in the inductive type
-   we're considering. *)
-
-let check_optim_id br =
-  let (kn,i) =
-    match br.(0) with (ConstructRef (c,_),_,_) -> c | _ -> assert false
-  in
-  let ip = (snd (lookup_ind kn)).ind_packets.(i) in
-  match ip.ip_optim_id_ok with
-    | Some ok -> ok
-    | None ->
-	let tvars =
-	  intset_union_map_array (intset_union_map_list type_listvar)
-	    ip.ip_types
-	in
-	let ok = (Intset.cardinal tvars = List.length ip.ip_vars) in
-	ip.ip_optim_id_ok <- Some ok;
-	ok
+  let br_factor, br_set = census_max MLdummy in
+  census_clean ();
+  let n = Intset.cardinal br_set in
+  if n = 0 then None
+  else if Array.length br >= 2 && n < 2 then None
+  else Some (br_factor, br_set)
 
 (*s If all branches are functions, try to permut the case and the functions. *)
 
@@ -897,26 +898,14 @@ and simpl_case o i br e =
     if n <> 0 then
       simpl o (named_lams ids (MLcase (i,ast_lift n e, br)))
     else
-      (* Does a term [f] exist such that many branches are [(f e)] ? *)
-      let opt1 =
-	if o.opt_case_idr && (o.opt_case_idg || check_optim_id br) then
-	  factor_branches check_function_branch br
-	else None
-      in
-      (* Detect common constant branches. Often a particular case of
-	 branch-as-function optim, but not always (e.g. A->A|B->A) *)
-      let opt2 =
-	if opt1 = None && o.opt_case_cst then
-	  factor_branches check_constant_branch br
-	else opt1
-      in
-      match opt2 with
-	| Some (f,ints) when List.length ints = Array.length br ->
-	    (* if all branches have been factorized, we remove the match *)
+      (* Can we merge several branches as the same constant or function ? *)
+      match factor_branches o i.m_typs br with
+	| Some (f,ints) when Intset.cardinal ints = Array.length br ->
+	    (* If all branches have been factorized, we remove the match *)
 	    simpl o (MLletin (Tmp anonymous_name, e, f))
 	| Some (f,ints) ->
-	    let ci = if ast_occurs 1 f then BranchFun ints else BranchCst ints
-	    in MLcase ((fst i,ci), e, br)
+	  let same = if ast_occurs 1 f then BranchFun ints else BranchCst ints
+	  in MLcase ({i with m_same=same}, e, br)
 	| None -> MLcase (i, e, br)
 
 (*S Local prop elimination. *)
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index d2ac48ea..6b0cd4f9 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mlutil.mli 13420 2010-09-16 15:47:08Z letouzey $ i*)
+(*i $Id: mlutil.mli 13733 2010-12-21 13:08:53Z letouzey $ i*)
 
 open Util
 open Names
@@ -63,6 +63,7 @@ val var2var' : ml_type -> ml_type
 type abbrev_map = global_reference -> ml_type option
 
 val type_expand : abbrev_map -> ml_type -> ml_type
+val type_simpl : ml_type -> ml_type
 val type_to_sign : abbrev_map -> ml_type -> sign
 val type_to_signature : abbrev_map -> ml_type -> signature
 val type_expunge : abbrev_map -> ml_type -> ml_type
@@ -116,8 +117,8 @@ val optimize_fix : ml_ast -> ml_ast
 val inline : global_reference -> ml_ast -> bool
 
 exception Impossible
-val check_function_branch : ml_branch -> ml_ast
-val check_constant_branch : ml_branch -> ml_ast
+val branch_as_fun : ml_type list -> ml_branch -> ml_ast
+val branch_as_cst : ml_branch -> ml_ast
 
 (* Classification of signatures *)
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index b4334750..313fc58d 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
+(*i $Id: modutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
 
 open Names
 open Declarations
@@ -82,10 +82,10 @@ let ast_iter_references do_term do_cons do_type a =
     match a with
       | MLglob r -> do_term r
       | MLcons (i,r,_) ->
-	  if lang () = Ocaml then record_iter_references do_term i;
+	  if lang () = Ocaml then record_iter_references do_term i.c_kind;
 	  do_cons r
       | MLcase (i,_,v) ->
-	  if lang () = Ocaml then record_iter_references do_term (fst i);
+	  if lang () = Ocaml then record_iter_references do_term i.m_kind;
 	  Array.iter (fun (r,_,_) -> do_cons r) v
       | _ -> ()
   in iter a
@@ -101,7 +101,7 @@ let ind_iter_references do_term do_cons do_type kn ind =
 	 | _ -> ());
     Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
   in
-  if lang () = Ocaml then record_iter_references do_term ind.ind_info;
+  if lang () = Ocaml then record_iter_references do_term ind.ind_kind;
     Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
 
 let decl_iter_references do_term do_cons do_type =
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 36ca3713..f136fab5 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ocaml.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: ocaml.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
 
 (*s Production of Ocaml syntax. *)
 
@@ -218,17 +218,17 @@ let rec pp_expr par env args =
         when kn = ind_ascii && check_extract_ascii () & is_list_cons l ->
 	assert (args=[]);
 	pp_char l
-    | MLcons (Coinductive,r,[]) ->
+    | MLcons ({c_kind = Coinductive},r,[]) ->
 	assert (args=[]);
 	pp_par par (str "lazy " ++ pp_global Cons r)
-    | MLcons (Coinductive,r,args') ->
+    | MLcons ({c_kind = Coinductive},r,args') ->
 	assert (args=[]);
 	let tuple = pp_tuple (pp_expr true env []) args' in
 	pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")")
     | MLcons (_,r,[]) ->
 	assert (args=[]);
 	pp_global Cons r
-    | MLcons (Record projs, r, args') ->
+    | MLcons ({c_kind = Record projs}, r, args') ->
 	assert (args=[]);
 	pp_record_pat (projs, List.map (pp_expr true env []) args')
     | MLcons (_,r,[arg1;arg2]) when is_infix r ->
@@ -250,14 +250,14 @@ let rec pp_expr par env args =
 	hov 2 (str (find_custom_match pv) ++ fnl () ++
 		 prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv
 	       ++ pp_expr true env [] t)
-    | MLcase ((i,factors), t, pv) ->
-	let expr = if i = Coinductive then
+    | MLcase (info, t, pv) ->
+	let expr = if info.m_kind = Coinductive then
 	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
 	else
 	  (pp_expr false env [] t)
 	in
 	(try
-	   let projs = find_projections i in
+	   let projs = find_projections info.m_kind in
 	   let (_, ids, c) = pv.(0) in
 	   let n = List.length ids in
 	   match c with
@@ -277,7 +277,7 @@ let rec pp_expr par env args =
 	     | _ -> raise NoRecord
 	 with NoRecord ->
 	   if Array.length pv = 1 then
-	     let s1,s2 = pp_one_pat env i pv.(0) in
+	     let s1,s2 = pp_one_pat env info pv.(0) in
 	     apply
 	       (hv 0
 		  (pp_par par'
@@ -291,7 +291,7 @@ let rec pp_expr par env args =
 		  (try pp_ifthenelse par' env expr pv
 		   with Not_found ->
 		     v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++
-			  str "  | " ++ pp_pat env (i,factors) pv))))
+			  str "  | " ++ pp_pat env info pv))))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
@@ -324,11 +324,11 @@ and pp_ifthenelse par env expr pv = match pv with
 	           hov 2 (pp_expr (expr_needs_par els) env [] els)))
   | _ -> raise Not_found
 
-and pp_one_pat env i (r,ids,t) =
+and pp_one_pat env info (r,ids,t) =
   let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
   let expr = pp_expr (expr_needs_par t) env' [] t in
   try
-    let projs = find_projections i in
+    let projs = find_projections info.m_kind in
     pp_record_pat (projs, List.rev_map pr_id ids), expr
   with NoRecord ->
     (match List.rev ids with
@@ -340,36 +340,42 @@ and pp_one_pat env i (r,ids,t) =
 	   ++ pp_boxed_tuple pr_id ids),
     expr
 
-and pp_pat env (info,factors) pv =
-  let factor_br, factor_l = try match factors with
-    | BranchFun (i::_ as l) -> check_function_branch pv.(i), l
-    | BranchCst (i::_ as l) -> ast_pop (check_constant_branch pv.(i)), l
-    | _ -> MLdummy, []
-  with Impossible -> MLdummy, []
+and pp_pat env info pv =
+  let factor_br, factor_set = try match info.m_same with
+    | BranchFun ints ->
+        let i = Intset.choose ints in
+        branch_as_fun info.m_typs pv.(i), ints
+    | BranchCst ints ->
+        let i = Intset.choose ints in
+	ast_pop (branch_as_cst pv.(i)), ints
+    | BranchNone -> MLdummy, Intset.empty
+  with _ -> MLdummy, Intset.empty
   in
-  let par = expr_needs_par factor_br in
   let last = Array.length pv - 1 in
   prvecti
-    (fun i x -> if List.mem i factor_l then mt () else
+    (fun i x -> if Intset.mem i factor_set then mt () else
        let s1,s2 = pp_one_pat env info x in
        hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++
-       if i = last && factor_l = [] then mt () else
+       if i = last && Intset.is_empty factor_set then mt () else
        fnl () ++ str "  | ") pv
   ++
-  if factor_l = [] then mt () else match factors with
+  if Intset.is_empty factor_set then mt () else
+  let par = expr_needs_par factor_br in
+  match info.m_same with
     | BranchFun _ ->
-	let ids, env' = push_vars [anonymous_name] env in
-	hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++
-	       pp_expr par env' [] factor_br)
+        let ids, env' = push_vars [anonymous_name] env in
+        hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++
+		 pp_expr par env' [] factor_br)
     | BranchCst _ ->
-	hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br)
+        hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br)
     | BranchNone -> mt ()
 
 and pp_function env t =
   let bl,t' = collect_lams t in
   let bl,env' = push_vars (List.map id_of_mlid bl) env in
   match t' with
-    | MLcase(i,MLrel 1,pv) when fst i=Standard && not (is_custom_match pv) ->
+    | MLcase(i,MLrel 1,pv) when
+	i.m_kind = Standard && not (is_custom_match pv) ->
 	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
 	  pr_binding (List.rev (List.tl bl)) ++
        	  str " = function" ++ fnl () ++
@@ -519,7 +525,7 @@ let pp_ind co kn ind =
 (*s Pretty-printing of a declaration. *)
 
 let pp_mind kn i =
-  match i.ind_info with
+  match i.ind_kind with
     | Singleton -> pp_singleton kn i.ind_packets.(0)
     | Coinductive -> pp_ind true kn i
     | Record projs ->
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index fa293ba1..06098591 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: scheme.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: scheme.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
 
 (*s Production of Scheme syntax. *)
 
@@ -87,7 +87,7 @@ let rec pp_expr env args =
 		    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
     | MLglob r ->
 	apply (pp_global Term r)
-    | MLcons (i,r,args') ->
+    | MLcons (info,r,args') ->
 	assert (args=[]);
 	let st =
 	  str "`" ++
@@ -95,7 +95,7 @@ let rec pp_expr env args =
 		 (if args' = [] then mt () else spc ()) ++
 		 prlist_with_sep spc (pp_cons_args env) args')
 	in
-	if i = Coinductive then paren (str "delay " ++ st) else st
+	if info.c_kind = Coinductive then paren (str "delay " ++ st) else st
     | MLcase (_,t,pv) when is_custom_match pv ->
 	let mkfun (_,ids,e) =
 	  if ids <> [] then named_lams (List.rev ids) e
@@ -104,9 +104,9 @@ let rec pp_expr env args =
 	hov 2 (str (find_custom_match pv) ++ fnl () ++
 		 prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv
 	       ++ pp_expr env [] t)
-     | MLcase ((i,_),t, pv) ->
+     | MLcase (info,t, pv) ->
 	let e =
-	  if i <> Coinductive then pp_expr env [] t
+	  if info.m_kind <> Coinductive then pp_expr env [] t
 	  else paren (str "force" ++ spc () ++ pp_expr env [] t)
 	in
 	apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
@@ -123,7 +123,7 @@ let rec pp_expr env args =
     | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
 
 and pp_cons_args env = function
-  | MLcons (i,r,args) when i<>Coinductive ->
+  | MLcons (info,r,args) when info.c_kind<>Coinductive ->
       paren (pp_global Cons r ++
 	     (if args = [] then mt () else spc ()) ++
 	     prlist_with_sep spc (pp_cons_args env) args)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a7e636ff..085c0a44 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
+(*i $Id: table.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
 
 open Names
 open Term
@@ -421,7 +421,8 @@ let flag_of_int n =
       opt_lin_beta = kth_digit n 10 }
 
 (* For the moment, we allow by default everything except :
-   - the type-unsafe optimization [opt_case_idg]
+   - the type-unsafe optimization [opt_case_idg], which anyway
+     cannot be activated currently (cf [Mlutil.branch_as_fun])
    - the linear let and beta reduction [opt_lin_let] and [opt_lin_beta]
      (may lead to complexity blow-up, subsumed by finer reductions
       when inlining recursors).
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index f1bdd640..3fb6824b 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -28,7 +28,7 @@ type oblinfo =
     ev_hyps: named_context;
     ev_status: obligation_definition_status;
     ev_chop: int option;
-    ev_loc: Util.loc;
+    ev_source: hole_kind located;
     ev_typ: types;
     ev_tac: tactic option;
     ev_deps: Intset.t }
@@ -218,9 +218,9 @@ let eterm_obligations env name isevars evm fs ?status t ty =
 	       else None
 	   | None -> None
 	 in
-	 let info = { ev_name = (n, nstr);
-		      ev_hyps = hyps; ev_status = status; ev_chop = chop;
-		      ev_loc = loc; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
+	 let info = { ev_name = (n, nstr); ev_hyps = hyps; 
+		      ev_status = status; ev_chop = chop;
+		      ev_source = (loc, k); ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
 	 in (id, info) :: l)
       evn []
   in
@@ -231,12 +231,12 @@ let eterm_obligations env name isevars evm fs ?status t ty =
   let evars = 
     List.map (fun (ev, info) ->
       let { ev_name = (_, name); ev_status = status;
-	    ev_loc = loc; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
+	    ev_source = source; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
       in
       let status = match status with
 	| Define true when Idset.mem name transparent -> Define false
 	| _ -> status
-      in name, typ, loc, status, deps, tac) evts
+      in name, typ, source, status, deps, tac) evts
   in
   let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
   let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
index 262889c8..2abc25a3 100644
--- a/plugins/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: eterm.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: eterm.mli 13693 2010-12-08 15:32:25Z msozeau $ i*)
 open Environ
 open Tacmach
 open Term
@@ -24,7 +24,7 @@ val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info *
    evars contexts, object and type *)
 val eterm_obligations : env -> identifier -> evar_map -> evar_map -> int ->
   ?status:obligation_definition_status -> constr -> types -> 
-  (identifier * types * loc * obligation_definition_status * Intset.t * 
+  (identifier * types * hole_kind located * obligation_definition_status * Intset.t * 
       tactic option) array
     (* Existential key, obl. name, type as product, location of the original evar, associated tactic,
        status and dependencies as indexes into the array *)
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index b76d0cb0..d3a63410 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -30,13 +30,13 @@ let explain_no_obligations = function
     Some ident -> str "No obligations for program " ++ str (string_of_id ident)
   | None -> str "No obligations remaining"
 
-type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t
-			 * tactic option) array
+type obligation_info = (Names.identifier * Term.types * hole_kind located * 
+			  obligation_definition_status * Intset.t * tactic option) array
 
 type obligation =
   { obl_name : identifier;
     obl_type : types;
-    obl_location : loc;
+    obl_source : hole_kind located;
     obl_body : constr option;
     obl_status : obligation_definition_status;
     obl_deps : Intset.t;
@@ -307,14 +307,14 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
 	assert(obls = [||]);
 	let n = Nameops.add_suffix n "_obligation" in
 	  [| { obl_name = n; obl_body = None;
-	       obl_location = dummy_loc; obl_type = t;
+	       obl_source = (dummy_loc, QuestionMark Expand); obl_type = t;
 	       obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |],
 	mkVar n
     | Some b ->
 	Array.mapi
 	  (fun i (n, t, l, o, d, tac) ->
             { obl_name = n ; obl_body = None; 
-	      obl_location = l; obl_type = reduce t; obl_status = o;
+	      obl_source = l; obl_type = reduce t; obl_status = o;
 	      obl_deps = d; obl_tac = tac })
 	  obls, b
   in
@@ -488,7 +488,7 @@ and solve_obligation_by_tac prg obls i tac =
 	| Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
 	| Stdpp.Exc_located(_, Refiner.FailError (_, s))
 	| Refiner.FailError (_, s) ->
-	    user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s)
+	    user_err_loc (fst obl.obl_source, "solve_obligation", Lazy.force s)
 	| e -> false
 
 and solve_prg_obligations prg tac =
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index bc5fc3e1..5f6d1a2e 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -6,9 +6,9 @@ open Proof_type
 open Vernacexpr
 
 type obligation_info =
-  (identifier * Term.types * loc *
+  (identifier * Term.types * hole_kind located *
       obligation_definition_status * Intset.t * tactic option) array
-    (* ident, type, location, (opaque or transparent, expand or define),
+    (* ident, type, source, (opaque or transparent, expand or define),
        dependencies, tactic to solve it *)
 
 type progress = (* Resolution status of a program *)