Imported Upstream version 8.3upstream/8.3

18 files changed, 238 insertions, 165 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 4171aceb..82b4143e 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ccalgo.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ccalgo.ml 13409 2010-09-13 07:53:13Z soubiran $ *)
 
 (* This file implements the basic congruence-closure algorithm by *)
 (* Downey,Sethi and Tarjan. *)
@@ -339,6 +339,28 @@ and make_app l=function
     Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1
   | other -> applistc (constr_of_term other) l
 
+let rec canonize_name c =
+  let func =  canonize_name in
+    match kind_of_term c with
+      | Const kn ->
+	  let canon_const = constant_of_kn (canonical_con kn) in 
+	    (mkConst canon_const)
+      | Ind (kn,i) ->
+	  let canon_mind = mind_of_kn (canonical_mind kn) in
+	    (mkInd (canon_mind,i))
+      | Construct ((kn,i),j) ->
+	  let canon_mind = mind_of_kn (canonical_mind kn) in
+	    mkConstruct ((canon_mind,i),j) 
+      | Prod (na,t,ct) ->
+	  mkProd (na,func t, func ct)
+      | Lambda (na,t,ct) ->
+	  mkLambda (na, func t,func ct)
+      | LetIn (na,b,t,ct) ->
+	  mkLetIn (na, func b,func t,func ct)
+      | App (ct,l) ->
+	  mkApp (func ct,array_smartmap func l)
+      | _ -> c
+
 (* rebuild a term from a pattern and a substitution *)
 
 let build_subst uf subst =
@@ -366,6 +388,7 @@ let rec add_term state t=
 	Not_found ->
 	  let b=next uf in
 	  let typ = pf_type_of state.gls (constr_of_term t) in
+	  let typ = canonize_name typ in
 	  let new_node=
 	    match t with
 		Symb _ | Product (_,_) ->
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b7358121..ca1a9085 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: cctac.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: cctac.ml 13409 2010-09-13 07:53:13Z soubiran $ *)
 
 (* This file is the interface between the c-c algorithm and Coq *)
 
@@ -74,11 +74,21 @@ let rec decompose_term env sigma t=
 		    decompose_term env sigma a),
 	      decompose_term env sigma b)
     | Construct c->
-	let (oib,_)=Global.lookup_inductive (fst c) in
-	let nargs=mis_constructor_nargs_env env c in
-	  Constructor {ci_constr=c;
+	let (mind,i_ind),i_con = c in 
+	let canon_mind = mind_of_kn (canonical_mind mind) in
+	let canon_ind = canon_mind,i_ind in
+	let (oib,_)=Global.lookup_inductive (canon_ind) in
+	let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in
+	  Constructor {ci_constr= (canon_ind,i_con);
 		       ci_arity=nargs;
 		       ci_nhyps=nargs-oib.mind_nparams}
+    | Ind c -> 
+	let mind,i_ind = c in 
+	let canon_mind = mind_of_kn (canonical_mind mind) in
+	let canon_ind = canon_mind,i_ind in  (Symb (mkInd canon_ind))
+    | Const c -> 
+	let canon_const = constant_of_kn (canonical_con c) in 
+	  (Symb (mkConst canon_const))
     | _ ->if closed0 t then (Symb t) else raise Not_found
 
 (* decompose equality in members and type *)
@@ -106,7 +116,7 @@ let rec pattern_of_constr env sigma c =
     | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
 	let b =pop _b in
 	let pa,sa = pattern_of_constr env sigma a in
-	let pb,sb = pattern_of_constr env sigma (pop b) in
+	let pb,sb = pattern_of_constr env sigma b in
 	let sort_b = sf_of env sigma b in
 	let sort_a = sf_of env sigma a in
 	  PApp(Product (sort_a,sort_b),
@@ -143,27 +153,27 @@ let patterns_of_constr env sigma nrels term=
 
 let rec quantified_atom_of_constr env sigma nrels term =
   match kind_of_term (whd_delta env term) with
-      Prod (_,atom,ff) ->
+      Prod (id,atom,ff) -> 
 	if eq_constr ff (Lazy.force _False) then
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
-	else
-	  quantified_atom_of_constr env sigma (succ nrels) ff
-    | _ ->
+	else 
+	  quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma (succ nrels) ff
+    | _ ->  
 	let patts=patterns_of_constr env sigma nrels term in
 	    `Rule patts
 
 let litteral_of_constr env sigma term=
   match kind_of_term (whd_delta env term) with
-    | Prod (_,atom,ff) ->
+    | Prod (id,atom,ff) -> 
 	if eq_constr ff (Lazy.force _False) then
 	  match (atom_of_constr env sigma atom) with
 	      `Eq(t,a,b) -> `Neq(t,a,b)
 	    | `Other(p) -> `Nother(p)
 	else
 	  begin
-	    try
-	      quantified_atom_of_constr env sigma 1 ff
+	    try 
+	      quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma 1 ff  
 	    with Not_found ->
 	      `Other (decompose_term env sigma term)
 	  end
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index ca72f873..8dc512fa 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: common.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: common.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
 
 open Pp
 open Util
@@ -177,6 +177,10 @@ let mktable autoclean =
 let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content =
   mktable false
 
+let get_mpfiles_content mp =
+  try get_mpfiles_content mp
+  with Not_found -> failwith "get_mpfiles_content"
+
 (*s The list of external modules that will be opened initially *)
 
 let mpfiles_add, mpfiles_mem, mpfiles_list, mpfiles_clear =
@@ -223,11 +227,13 @@ let pop_visible, push_visible, get_visible =
   let vis = ref [] in
   register_cleanup (fun () -> vis := []);
   let pop () =
-    let v = List.hd !vis in
-    (* we save the 1st-level-content of MPfile for later use *)
-    if get_phase () = Impl && modular () && is_modfile v.mp
-    then add_mpfiles_content v.mp v.content;
-    vis := List.tl !vis
+    match !vis with
+      | [] -> assert false
+      | v :: vl ->
+	  vis := vl;
+	  (* we save the 1st-level-content of MPfile for later use *)
+	  if get_phase () = Impl && modular () && is_modfile v.mp
+	  then add_mpfiles_content v.mp v.content
   and push mp mps =
     vis := { mp = mp; params = mps; content = Hashtbl.create 97 } :: !vis
   and get () = !vis
@@ -306,8 +312,8 @@ let rec mp_renaming_fun mp = match mp with
       let s = modular_rename Mod (id_of_mbid mbid) in
       if not (params_ren_mem mp) then [s]
       else let i,_,_ = repr_mbid mbid in [s^"__"^string_of_int i]
-  | MPfile _ when not (modular ()) -> assert false (* see [at_toplevel] above *)
   | MPfile _ ->
+      assert (modular ()); (* see [at_toplevel] above *)
       assert (get_phase () = Pre);
       let current_mpfile = (list_last (get_visible ())).mp in
       if mp <> current_mpfile then mpfiles_add mp;
@@ -402,27 +408,28 @@ let visible_clash_dbg mp0 ks =
 let opened_libraries () =
   if not (modular ()) then []
   else
-    let used = mpfiles_list () in
-    let rec check_elsewhere avoid = function
-      | [] -> []
-      | mp :: mpl ->
-	  let clash s = Hashtbl.mem (get_mpfiles_content mp) (Mod,s) in
-	  if List.exists clash avoid
-	  then check_elsewhere avoid mpl
-	  else mp :: check_elsewhere (string_of_modfile mp :: avoid) mpl
+    let used_files = mpfiles_list () in
+    let used_ks = List.map (fun mp -> Mod,string_of_modfile mp) used_files in
+    (* By default, we open all used files. Ambiguities will be resolved later
+       by using qualified names. Nonetheless, we don't open any file A that
+       contains an immediate submodule A.B hiding another file B : otherwise,
+       after such an open, there's no unambiguous way to refer to objects of B. *)
+    let to_open =
+      List.filter
+	(fun mp ->
+	   not (List.exists (Hashtbl.mem (get_mpfiles_content mp)) used_ks))
+	used_files
     in
-    let opened = check_elsewhere [] used in
     mpfiles_clear ();
-    List.iter mpfiles_add opened;
-    opened
+    List.iter mpfiles_add to_open;
+    mpfiles_list ()
 
 (*s On-the-fly qualification issues for both monolithic or modular extraction. *)
 
-(* First, a function that factorize the printing of both [global_reference]
-   and module names for ocaml. When [k=Mod] then [olab=None], otherwise it
-   contains the label of the reference to print.
-   [rls] is the string list giving the qualified name, short name at the end.
-   Invariant: [List.length rls >= 2], simpler situations are handled elsewhere. *)
+(* [pp_ocaml_gen] below is a function that factorize the printing of both
+   [global_reference] and module names for ocaml. When [k=Mod] then [olab=None],
+   otherwise it contains the label of the reference to print.
+   [rls] is the string list giving the qualified name, short name at the end. *)
 
 (* In Coq, we can qualify [M.t] even if we are inside [M], but in Ocaml we
    cannot do that. So, if [t] gets hidden and we need a long name for it,
@@ -471,18 +478,21 @@ let pp_ocaml_bound base rls =
 (* [pp_ocaml_extern] : [mp] isn't local, it is defined in another [MPfile]. *)
 
 let pp_ocaml_extern k base rls = match rls with
-  | [] | [_] -> assert false
+  | [] -> assert false
   | base_s :: rls' ->
-      let k's = fstlev_ks k rls' in
-      if modular () && (mpfiles_mem base) &&
-	(not (mpfiles_clash base k's)) &&
-	(not (visible_clash base k's))
-      then (* Standard situation of an object in another file: *)
-	(* Thanks to the "open" of this file we remove its name *)
+      if (not (modular ())) (* Pseudo qualification with "" *)
+	|| (rls' = [])  (* Case of a file A.v used as a module later *)
+	|| (not (mpfiles_mem base)) (* Module not opened *)
+	|| (mpfiles_clash base (fstlev_ks k rls')) (* Conflict in opened files *)
+	|| (visible_clash base (fstlev_ks k rls')) (* Local conflict *)
+      then
+	(* We need to fully qualify. Last clash situation is unsupported *)
+	match visible_clash_dbg base (Mod,base_s) with
+	  | None -> dottify rls
+	  | Some (mp,l) -> error_module_clash base (MPdot (mp,l))
+      else
+	(* Standard situation : object in an opened file *)
 	dottify rls'
-      else match visible_clash_dbg base (Mod,base_s) with
-	| None -> dottify rls
-	| Some (mp,l) -> error_module_clash base (MPdot (mp,l))
 
 (* [pp_ocaml_gen] : choosing between [pp_ocaml_extern] or [pp_ocaml_extern] *)
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 58d8fcb1..c5929392 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extract_env.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: extract_env.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
 
 open Term
 open Declarations
@@ -69,7 +69,7 @@ module type VISIT = sig
 
   (* Add kernel_name / constant / reference / ... in the visit lists.
      These functions silently add the mp of their arg in the mp list *)
-  val add_kn : mutual_inductive -> unit
+  val add_ind : mutual_inductive -> unit
   val add_con : constant -> unit
   val add_ref : global_reference -> unit
   val add_decl_deps : ml_decl -> unit
@@ -77,31 +77,35 @@ module type VISIT = sig
 
   (* Test functions:
      is a particular object a needed dependency for the current extraction ? *)
-  val needed_kn : mutual_inductive -> bool
+  val needed_ind : mutual_inductive -> bool
   val needed_con : constant -> bool
   val needed_mp : module_path -> bool
 end
 
 module Visit : VISIT = struct
   (* What used to be in a single KNset should now be split into a KNset
-     (for inductives and modules names) and a Cset for constants
+     (for inductives and modules names) and a Cset_env for constants
      (and still the remaining MPset) *)
   type must_visit =
-      { mutable kn : Mindset.t; mutable con : Cset.t; mutable mp : MPset.t }
+      { mutable ind : KNset.t; mutable con : KNset.t; mutable mp : MPset.t }
   (* the imperative internal visit lists *)
-  let v = { kn = Mindset.empty ; con = Cset.empty ; mp = MPset.empty }
+  let v = { ind = KNset.empty ; con = KNset.empty ; mp = MPset.empty }
   (* the accessor functions *)
-  let reset () = v.kn <- Mindset.empty; v.con <- Cset.empty; v.mp <- MPset.empty
-  let needed_kn kn = Mindset.mem kn v.kn
-  let needed_con c = Cset.mem c v.con
+  let reset () = v.ind <- KNset.empty; v.con <- KNset.empty; v.mp <- MPset.empty
+  let needed_ind i = KNset.mem (user_mind i) v.ind
+  let needed_con c = KNset.mem (user_con c) v.con
   let needed_mp mp = MPset.mem mp v.mp
   let add_mp mp =
     check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp
-  let add_kn kn = v.kn <- Mindset.add kn v.kn; add_mp (mind_modpath kn)
-  let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c)
+  let add_ind i =
+    let kn = user_mind i in
+    v.ind <- KNset.add kn v.ind; add_mp (modpath kn)
+  let add_con c =
+    let kn = user_con c in
+    v.con <- KNset.add kn v.con; add_mp (modpath kn)
   let add_ref = function
     | ConstRef c -> add_con c
-    | IndRef (kn,_) | ConstructRef ((kn,_),_) -> add_kn kn
+    | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_ind ind
     | VarRef _ -> assert false
   let add_decl_deps = decl_iter_references add_ref add_ref add_ref
   let add_spec_deps = spec_iter_references add_ref add_ref add_ref
@@ -280,7 +284,7 @@ let rec extract_sfb env mp all = function
       let ms = extract_sfb env mp all msb in
       let kn = make_kn mp empty_dirpath l in
       let mind = mind_of_kn kn in
-      let b = Visit.needed_kn mind in
+      let b = Visit.needed_ind mind in
       if all || b then
 	let d = Dind (kn, extract_inductive env mind) in
 	if (not b) && (logical_decl d) then ms
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 057057d1..b615955f 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 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: extraction.ml 13427 2010-09-17 17:37:52Z letouzey $ i*)
 
 (*i*)
 open Util
@@ -817,6 +817,18 @@ let rec decomp_lams_eta_n n m env c t =
   let eta_args = List.rev_map mkRel (interval 1 d) in
   rels, applist (lift d c,eta_args)
 
+(* Let's try to identify some situation where extracted code
+   will allow generalisation of type variables *)
+
+let rec gentypvar_ok c = match kind_of_term c with
+  | Lambda _ | Const _ -> true
+  | App (c,v) ->
+      (* if all arguments are variables, these variables will
+	 disappear after extraction (see [empty_s] below) *)
+      array_for_all isRel v && gentypvar_ok c
+  | Cast (c,_,_) -> gentypvar_ok c
+  | _ -> false
+
 (*s From a constant to a ML declaration. *)
 
 let extract_std_constant env kn body typ =
@@ -846,6 +858,17 @@ let extract_std_constant env kn body typ =
       then decompose_lam_n m body
       else decomp_lams_eta_n n m env body typ
   in
+  (* Should we do one eta-expansion to avoid non-generalizable '_a ? *)
+  let rels, c =
+    let n = List.length rels in
+    let s,s' = list_split_at n s in
+    let k = sign_kind s in
+    let empty_s = (k = EmptySig || k = SafeLogicalSig) in
+    if lang () = Ocaml && empty_s && not (gentypvar_ok c)
+      && s' <> [] && type_maxvar t <> 0
+    then decomp_lams_eta_n (n+1) n env body typ
+    else rels,c
+  in
   let n = List.length rels in
   let s = list_firstn n s in
   let l,l' = list_split_at n l in
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 57b7c365..29d3da4d 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 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: haskell.ml 13414 2010-09-14 13:28:15Z glondu $ i*)
 
 (*s Production of Haskell syntax. *)
 
@@ -297,7 +297,7 @@ let pp_decl = function
 	  try
 	    let ids,s = find_type_custom r in
 	    prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
-	  with not_found ->
+	  with Not_found ->
 	    prlist (fun id -> pr_id id ++ str " ") l ++
 	    if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
 	    else str "=" ++ spc () ++ pp_type false l t
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 745a78fe..a079aacc 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 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: mlutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
 
 (*i*)
 open Pp
@@ -656,10 +656,10 @@ let rec tmp_head_lams = function
 let rec ast_glob_subst s t = match t with
   | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) ->
       let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in
-      (try linear_beta_red a (Refmap.find refe s)
+      (try linear_beta_red a (Refmap'.find refe s)
        with Not_found -> MLapp (f, a))
   | MLglob ((ConstRef kn) as refe) ->
-      (try Refmap.find refe s with Not_found -> t)
+      (try Refmap'.find refe s with Not_found -> t)
   | _ -> ast_map (ast_glob_subst s) t
 
 
@@ -1259,7 +1259,7 @@ let con_of_string s =
     | [] -> assert false
 
 let manual_inline_set =
-  List.fold_right (fun x -> Cset.add (con_of_string x))
+  List.fold_right (fun x -> Cset_env.add (con_of_string x))
     [ "Coq.Init.Wf.well_founded_induction_type";
       "Coq.Init.Wf.well_founded_induction";
       "Coq.Init.Wf.Acc_iter";
@@ -1271,10 +1271,10 @@ let manual_inline_set =
       "Coq.Init.Logic.eq_rect_r";
       "Coq.Init.Specif.proj1_sig";
     ]
-    Cset.empty
+    Cset_env.empty
 
 let manual_inline = function
-  | ConstRef c -> Cset.mem c manual_inline_set
+  | ConstRef c -> Cset_env.mem c manual_inline_set
   | _ -> false
 
 (* If the user doesn't say he wants to keep [t], we inline in two cases:
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index d6b85f12..d2ac48ea 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -6,13 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mlutil.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: mlutil.mli 13420 2010-09-16 15:47:08Z letouzey $ i*)
 
 open Util
 open Names
 open Term
 open Libnames
 open Miniml
+open Table
 
 (*s Utility functions over ML types with meta. *)
 
@@ -108,7 +109,7 @@ val ast_lift : int -> ml_ast -> ml_ast
 val ast_pop : ml_ast -> ml_ast
 val ast_subst : ml_ast -> ml_ast -> ml_ast
 
-val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast
+val ast_glob_subst : ml_ast Refmap'.t -> ml_ast -> ml_ast
 
 val normalize : ml_ast -> ml_ast
 val optimize_fix : ml_ast -> ml_ast
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 15145344..b4334750 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 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: modutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
 
 open Names
 open Declarations
@@ -217,45 +217,25 @@ let get_decl_in_structure r struc =
 let dfix_to_mlfix rv av i =
   let rec make_subst n s =
     if n < 0 then s
-    else make_subst (n-1) (Refmap.add rv.(n) (n+1) s)
+    else make_subst (n-1) (Refmap'.add rv.(n) (n+1) s)
   in
-  let s = make_subst (Array.length rv - 1) Refmap.empty
+  let s = make_subst (Array.length rv - 1) Refmap'.empty
   in
   let rec subst n t = match t with
     | MLglob ((ConstRef kn) as refe) ->
-	(try MLrel (n + (Refmap.find refe s)) with Not_found -> t)
+	(try MLrel (n + (Refmap'.find refe s)) with Not_found -> t)
     | _ -> ast_map_lift subst n t
   in
   let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in
   let c = Array.map (subst 0) av
   in MLfix(i, ids, c)
 
-let rec optim to_appear s = function
-  | [] -> []
-  | (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l ->
-      if List.mem r to_appear
-      then d :: (optim to_appear s l)
-      else optim to_appear s l
-  | Dterm (r,t,typ) :: l ->
-      let t = normalize (ast_glob_subst !s t) in
-      let i = inline r t in
-      if i then s := Refmap.add r t !s;
-      if not i || modular () || List.mem r to_appear
-      then
-	let d = match optimize_fix t with
-	  | MLfix (0, _, [|c|]) ->
-	      Dfix ([|r|], [|ast_subst (MLglob r) c|], [|typ|])
-	  | t -> Dterm (r, t, typ)
-	in d :: (optim to_appear s l)
-      else optim to_appear s l
-  | d :: l -> d :: (optim to_appear s l)
-
 let rec optim_se top to_appear s = function
   | [] -> []
   | (l,SEdecl (Dterm (r,a,t))) :: lse ->
       let a = normalize (ast_glob_subst !s a) in
       let i = inline r a in
-      if i then s := Refmap.add r a !s;
+      if i then s := Refmap'.add r a !s;
       if top && i && not (modular ()) && not (List.mem r to_appear)
       then optim_se top to_appear s lse
       else
@@ -271,7 +251,7 @@ let rec optim_se top to_appear s = function
       let fake_body = MLfix (0,[||],[||]) in
       for i = 0 to Array.length rv - 1 do
 	if inline rv.(i) fake_body
-	then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s
+	then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s
 	else all := false
       done;
       if !all && top && not (modular ())
@@ -302,11 +282,11 @@ let base_r = function
   | _ -> assert false
 
 let reset_needed, add_needed, found_needed, is_needed =
-  let needed = ref Refset.empty in
-  ((fun l -> needed := Refset.empty),
-   (fun r -> needed := Refset.add (base_r r) !needed),
-   (fun r -> needed := Refset.remove (base_r r) !needed),
-   (fun r -> Refset.mem (base_r r) !needed))
+  let needed = ref Refset'.empty in
+  ((fun l -> needed := Refset'.empty),
+   (fun r -> needed := Refset'.add (base_r r) !needed),
+   (fun r -> needed := Refset'.remove (base_r r) !needed),
+   (fun r -> Refset'.mem (base_r r) !needed))
 
 let declared_refs = function
   | Dind (kn,_) -> [|IndRef (mind_of_kn kn,0)|]
@@ -361,7 +341,7 @@ let check_implicits = function
   | _ -> false
 
 let optimize_struct to_appear struc =
-  let subst = ref (Refmap.empty : ml_ast Refmap.t) in
+  let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in
   let opt_struc =
     List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
   in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index fd640388..a7e636ff 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 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: table.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
 
 open Names
 open Term
@@ -21,6 +21,13 @@ open Util
 open Pp
 open Miniml
 
+(** Sets and maps for [global_reference] that do _not_ work modulo
+    name equivalence (otherwise use Refset / Refmap ) *)
+
+module RefOrd = struct type t = global_reference let compare = compare end
+module Refmap' = Map.Make(RefOrd)
+module Refset' = Set.Make(RefOrd)
+
 (*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
 
 let occur_kn_in_ref kn = function
@@ -119,37 +126,47 @@ let rec add_labels_mp mp = function
 
 (*s Constants tables. *)
 
-let terms = ref (Cmap.empty : ml_decl Cmap.t)
-let init_terms () = terms := Cmap.empty
-let add_term kn d = terms := Cmap.add kn d !terms
-let lookup_term kn = Cmap.find kn !terms
+let terms = ref (Cmap_env.empty : ml_decl Cmap_env.t)
+let init_terms () = terms := Cmap_env.empty
+let add_term kn d = terms := Cmap_env.add kn d !terms
+let lookup_term kn = Cmap_env.find kn !terms
 
-let types = ref (Cmap.empty : ml_schema Cmap.t)
-let init_types () = types := Cmap.empty
-let add_type kn s = types := Cmap.add kn s !types
-let lookup_type kn = Cmap.find kn !types
+let types = ref (Cmap_env.empty : ml_schema Cmap_env.t)
+let init_types () = types := Cmap_env.empty
+let add_type kn s = types := Cmap_env.add kn s !types
+let lookup_type kn = Cmap_env.find kn !types
 
 (*s Inductives table. *)
 
-let inductives = ref (Mindmap.empty : (mutual_inductive_body * ml_ind) Mindmap.t)
-let init_inductives () = inductives := Mindmap.empty
-let add_ind kn mib ml_ind = inductives := Mindmap.add kn (mib,ml_ind) !inductives
-let lookup_ind kn = Mindmap.find kn !inductives
+let inductives =
+  ref (Mindmap_env.empty : (mutual_inductive_body * ml_ind) Mindmap_env.t)
+let init_inductives () = inductives := Mindmap_env.empty
+let add_ind kn mib ml_ind =
+  inductives := Mindmap_env.add kn (mib,ml_ind) !inductives
+let lookup_ind kn = Mindmap_env.find kn !inductives
 
 (*s Recursors table. *)
 
+(* NB: here we can use the equivalence between canonical
+   and user constant names : Cset is fine, no need for [Cset_env] *)
+
 let recursors = ref Cset.empty
 let init_recursors () = recursors := Cset.empty
 
 let add_recursors env kn =
-  let make_kn id = make_con (mind_modpath kn) empty_dirpath (label_of_id id) in
+  let mk_con id =
+    make_con_equiv
+      (modpath (user_mind kn))
+      (modpath (canonical_mind kn))
+      empty_dirpath (label_of_id id)
+  in
   let mib = Environ.lookup_mind kn env in
   Array.iter
     (fun mip ->
        let id = mip.mind_typename in
-       let kn_rec = make_kn (Nameops.add_suffix id "_rec")
-       and kn_rect = make_kn (Nameops.add_suffix id "_rect") in
-       recursors := Cset.add kn_rec (Cset.add kn_rect !recursors))
+       let c_rec = mk_con (Nameops.add_suffix id "_rec")
+       and c_rect = mk_con (Nameops.add_suffix id "_rect") in
+       recursors := Cset.add c_rec (Cset.add c_rect !recursors))
     mib.mind_packets
 
 let is_recursor = function
@@ -158,6 +175,8 @@ let is_recursor = function
 
 (*s Record tables. *)
 
+(* NB: here, working modulo name equivalence is ok *)
+
 let projs = ref (Refmap.empty : int Refmap.t)
 let init_projs () = projs := Refmap.empty
 let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs
@@ -166,12 +185,12 @@ let projection_arity r = Refmap.find r !projs
 
 (*s Table of used axioms *)
 
-let info_axioms = ref Refset.empty
-let log_axioms = ref Refset.empty
-let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty
-let add_info_axiom r = info_axioms := Refset.add r !info_axioms
-let remove_info_axiom r = info_axioms := Refset.remove r !info_axioms
-let add_log_axiom r = log_axioms := Refset.add r !log_axioms
+let info_axioms = ref Refset'.empty
+let log_axioms = ref Refset'.empty
+let init_axioms () = info_axioms := Refset'.empty; log_axioms := Refset'.empty
+let add_info_axiom r = info_axioms := Refset'.add r !info_axioms
+let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms
+let add_log_axiom r = log_axioms := Refset'.add r !log_axioms
 
 (*s Extraction mode: modular or monolithic *)
 
@@ -220,7 +239,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 let err s = errorlabstrm "Extraction" s
 
 let warning_axioms () =
-  let info_axioms = Refset.elements !info_axioms in
+  let info_axioms = Refset'.elements !info_axioms in
   if info_axioms = [] then ()
   else begin
     let s = if List.length info_axioms = 1 then "axiom" else "axioms" in
@@ -229,7 +248,7 @@ let warning_axioms () =
        ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
        ++ str "." ++ fnl ())
   end;
-  let log_axioms = Refset.elements !log_axioms in
+  let log_axioms = Refset'.elements !log_axioms in
   if log_axioms = [] then ()
   else begin
     let s = if List.length log_axioms = 1 then "axiom was" else "axioms were"
@@ -457,16 +476,16 @@ let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
 (*s Extraction Inline/NoInline *)
 
-let empty_inline_table = (Refset.empty,Refset.empty)
+let empty_inline_table = (Refset'.empty,Refset'.empty)
 
 let inline_table = ref empty_inline_table
 
-let to_inline r = Refset.mem r (fst !inline_table)
+let to_inline r = Refset'.mem r (fst !inline_table)
 
-let to_keep r = Refset.mem r (snd !inline_table)
+let to_keep r = Refset'.mem r (snd !inline_table)
 
 let add_inline_entries b l =
-  let f b = if b then Refset.add else Refset.remove in
+  let f b = if b then Refset'.add else Refset'.remove in
   let i,k = !inline_table in
   inline_table :=
   (List.fold_right (f b) l i),
@@ -504,14 +523,14 @@ let extraction_inline b l =
 
 let print_extraction_inline () =
   let (i,n)= !inline_table in
-  let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in
+  let i'= Refset'.filter (function ConstRef _ -> true | _ -> false) i in
   msg
     (str "Extraction Inline:" ++ fnl () ++
-     Refset.fold
+     Refset'.fold
        (fun r p ->
 	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++
      str "Extraction NoInline:" ++ fnl () ++
-     Refset.fold
+     Refset'.fold
        (fun r p ->
 	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) n (mt ()))
 
@@ -529,10 +548,10 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 type int_or_id = ArgInt of int | ArgId of identifier
 
-let implicits_table = ref Refmap.empty
+let implicits_table = ref Refmap'.empty
 
 let implicits_of_global r =
- try Refmap.find r !implicits_table with Not_found -> []
+ try Refmap'.find r !implicits_table with Not_found -> []
 
 let add_implicits r l =
   let typ = Global.type_of_global r in
@@ -552,7 +571,7 @@ let add_implicits r l =
 		safe_pr_global r))
   in
   let l' = List.map check l in
-  implicits_table := Refmap.add r l' !implicits_table
+  implicits_table := Refmap'.add r l' !implicits_table
 
 (* Registration of operations for rollback. *)
 
@@ -568,7 +587,7 @@ let (implicit_extraction,_) =
 let _ = declare_summary "Extraction Implicit"
 	  { freeze_function = (fun () -> !implicits_table);
 	    unfreeze_function = ((:=) implicits_table);
-	    init_function = (fun () -> implicits_table := Refmap.empty) }
+	    init_function = (fun () -> implicits_table := Refmap'.empty) }
 
 (* Grammar entries. *)
 
@@ -658,22 +677,22 @@ let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 let use_type_scheme_nb_args, register_type_scheme_nb_args =
   let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r
 
-let customs = ref Refmap.empty
+let customs = ref Refmap'.empty
 
-let add_custom r ids s = customs := Refmap.add r (ids,s) !customs
+let add_custom r ids s = customs := Refmap'.add r (ids,s) !customs
 
-let is_custom r = Refmap.mem r !customs
+let is_custom r = Refmap'.mem r !customs
 
 let is_inline_custom r = (is_custom r) && (to_inline r)
 
-let find_custom r = snd (Refmap.find r !customs)
+let find_custom r = snd (Refmap'.find r !customs)
 
-let find_type_custom r = Refmap.find r !customs
+let find_type_custom r = Refmap'.find r !customs
 
-let custom_matchs = ref Refmap.empty
+let custom_matchs = ref Refmap'.empty
 
 let add_custom_match r s =
-  custom_matchs := Refmap.add r s !custom_matchs
+  custom_matchs := Refmap'.add r s !custom_matchs
 
 let indref_of_match pv =
   if Array.length pv = 0 then raise Not_found;
@@ -682,11 +701,11 @@ let indref_of_match pv =
     | _ -> raise Not_found
 
 let is_custom_match pv =
-  try Refmap.mem (indref_of_match pv) !custom_matchs
+  try Refmap'.mem (indref_of_match pv) !custom_matchs
   with Not_found -> false
 
 let find_custom_match pv =
-  Refmap.find (indref_of_match pv) !custom_matchs
+  Refmap'.find (indref_of_match pv) !custom_matchs
 
 (* Registration of operations for rollback. *)
 
@@ -703,7 +722,7 @@ let (in_customs,_) =
 let _ = declare_summary "ML extractions"
 	  { freeze_function = (fun () -> !customs);
 	    unfreeze_function = ((:=) customs);
-	    init_function = (fun () -> customs := Refmap.empty) }
+	    init_function = (fun () -> customs := Refmap'.empty) }
 
 let (in_custom_matchs,_) =
   declare_object
@@ -717,7 +736,7 @@ let (in_custom_matchs,_) =
 let _ = declare_summary "ML extractions custom match"
 	  { freeze_function = (fun () -> !custom_matchs);
 	    unfreeze_function = ((:=) custom_matchs);
-	    init_function = (fun () -> custom_matchs := Refmap.empty) }
+	    init_function = (fun () -> custom_matchs := Refmap'.empty) }
 
 (* Grammar entries. *)
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index a3199b50..ff4780a1 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -6,13 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: table.mli 13420 2010-09-16 15:47:08Z letouzey $ i*)
 
 open Names
 open Libnames
 open Miniml
 open Declarations
 
+module Refset' : Set.S with type elt = global_reference
+module Refmap' : Map.S with type key = global_reference
+
 val safe_basename_of_global : global_reference -> identifier
 
 (*s Warning and Error messages. *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index d287913d..e47f19bf 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -235,7 +235,7 @@ let warning_error names e =
 	  (str "Cannot define principle(s) for "++
 	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
 	     if do_observe () then Cerrors.explain_exn e else mt ())
-    | _ -> anomaly ""
+    | _ -> raise e
 
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
@@ -263,11 +263,11 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
 		  end
 	      | _ -> assert false (* we can only have non empty  list *)
 	  end
-    	  | e ->
+	  | e -> 
 	      let names = List.map (fun (_,na,_) -> na) fas in
 	      warning_error names e
-
       end
+
     ]
 END
 (***** debug only ***)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f5a5fbd4..a61671f8 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -294,7 +294,7 @@ let warning_error names e =
 	  (str "Cannot define principle(s) for "++
 	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
 	     e_explain e)
-    | _ -> anomaly ""
+    | _ -> raise e
 
 let error_error names e =
   let e_explain e =
@@ -308,7 +308,7 @@ let error_error names e =
 	  (str "Cannot define graph(s) for " ++
 	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
 	     e_explain e)
-    | _ -> anomaly ""
+    | _ -> raise e
 
 let generate_principle  on_error
     is_general do_built fix_rec_l recdefs  interactive_proof
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a980d963..6376d023 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1434,7 +1434,7 @@ let micromega_gen
       (" Skipping what remains of this tactic: the complexity of the goal requires "
       ^ "the use of a specialized external tool called csdp. \n\n" 
       ^ "Unfortunately this instance of Coq isn't aware of the presence of any \"csdp\" executable. \n\n"
-      ^ "You may need to specify the location during Coq's pre-compilation configuration step")) gl
+      ^ "This executable should be in PATH")) gl
 
 let lift_ratproof  prover l =
  match prover l with
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 885f7fb6..90b409ba 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac.ml 13344 2010-07-28 15:04:36Z msozeau $ *)
+(* $Id: subtac.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
 
 open Global
 open Pp
@@ -80,7 +80,7 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
   in
   let c = solve_tccs_in_type env id isevars evm c typ in
     Lemmas.start_proof id kind c (fun loc gr ->
-      Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true imps;
+      Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps];
       hook loc gr)
 
 let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index b2bf9912..4927adbe 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtac_classes.ml 13328 2010-07-26 11:05:30Z herbelin $ i*)
+(*i $Id: subtac_classes.ml 13516 2010-10-07 19:09:38Z msozeau $ i*)
 
 open Pretyping
 open Evd
@@ -123,7 +123,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
     match props with
     | Inr term ->
 	let c = interp_casted_constr_evars evars env' term cty in
-	  Inr (c, subst)
+	  Inr c
     | Inl props ->
 	let get_id =
 	  function
@@ -162,7 +162,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
 	let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in
 	  term, termtype
-    | Inr (def, subst) ->
+    | Inr def ->
 	let termtype = it_mkProd_or_LetIn cty ctx in
 	let term = Termops.it_mkLambda_or_LetIn def ctx in
 	  term, termtype
@@ -174,7 +174,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   let hook vis gr =
     let cst = match gr with ConstRef kn -> kn | _ -> assert false in
     let inst = Typeclasses.new_instance k pri global (ConstRef cst) in
-      Impargs.declare_manual_implicits false gr ~enriching:false imps;
+      Impargs.declare_manual_implicits false gr ~enriching:false [imps];
       Typeclasses.add_instance inst
   in
   let evm = Subtac_utils.evars_of_term !evars Evd.empty term in
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index e7dd7ef1..a83611a4 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -333,7 +333,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
 	  if Impargs.is_implicit_args () || impls <> [] then
-	    Impargs.declare_manual_implicits false gr impls
+	    Impargs.declare_manual_implicits false gr [impls]
       in
       let typ = it_mkProd_or_LetIn top_arity binders in
 	hook, name, typ
@@ -341,7 +341,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
       let typ = it_mkProd_or_LetIn top_arity binders_rel in
       let hook l gr = 
 	if Impargs.is_implicit_args () || impls <> [] then
-	  Impargs.declare_manual_implicits false gr impls
+	  Impargs.declare_manual_implicits false gr [impls]
       in hook, recname, typ
   in
   let fullcoqc = Evarutil.nf_evar !isevars def in
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 1424618f..b76d0cb0 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -211,7 +211,7 @@ let declare_definition prg =
 	in
 	let gr = ConstRef c in
 	  if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
-	    Impargs.declare_manual_implicits false gr prg.prg_implicits;
+	    Impargs.declare_manual_implicits false gr [prg.prg_implicits];
 	  print_message (Subtac_utils.definition_message prg.prg_name);
 	  progmap_remove prg; 
 	  prg.prg_hook local gr;