Imported Upstream version 8.0pl1upstream/8.0pl1

21 files changed, 6288 insertions, 0 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
new file mode 100644
index 00000000..6692dca5
--- /dev/null
+++ b/interp/constrextern.ml
@@ -0,0 +1,1855 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: constrextern.ml,v 1.85.2.2 2004/07/16 19:30:22 herbelin Exp $ *)
+
+(*i*)
+open Pp
+open Util
+open Univ
+open Names
+open Nameops
+open Term
+open Termops
+open Inductive
+open Sign
+open Environ
+open Libnames
+open Impargs
+open Topconstr
+open Rawterm
+open Pattern
+open Nametab
+open Symbols
+open Reserve
+(*i*)
+
+(* Translation from rawconstr to front constr *)
+
+(**********************************************************************)
+(* Parametrization                                                    *)
+
+(* This governs printing of local context of references *)
+let print_arguments = ref false
+
+(* If true, prints local context of evars, whatever print_arguments *)
+let print_evar_arguments = ref false
+
+(* This governs printing of implicit arguments.  When
+   [print_implicits] is on then [print_implicits_explicit_args] tells
+   how implicit args are printed. If on, implicit args are printed
+   prefixed by "!" otherwise the function and not the arguments is
+   prefixed by "!" *)
+let print_implicits = ref false
+let print_implicits_explicit_args = ref false
+
+(* This forces printing of coercions *)
+let print_coercions = ref false
+
+(* This forces printing universe names of Type{.} *)
+let print_universes = ref false
+
+(* This suppresses printing of numeral and symbols *)
+let print_no_symbol = ref false
+
+(* This governs printing of projections using the dot notation symbols *)
+let print_projections = ref false
+
+let print_meta_as_hole = ref false
+
+let with_arguments f = Options.with_option print_arguments f
+let with_implicits f = Options.with_option print_implicits f
+let with_coercions f = Options.with_option print_coercions f
+let with_universes f = Options.with_option print_universes f
+let without_symbols f = Options.with_option print_no_symbol f
+let with_meta_as_hole f = Options.with_option print_meta_as_hole f
+
+(* For the translator *)
+let temporary_implicits_out = ref []
+let set_temporary_implicits_out l = temporary_implicits_out := l
+let get_temporary_implicits_out id =
+  try List.assoc id !temporary_implicits_out
+  with Not_found -> []
+
+(**********************************************************************)
+(* Various externalisation functions *)
+
+let insert_delimiters e = function
+  | None -> e
+  | Some sc -> CDelimiters (dummy_loc,sc,e)
+
+let insert_pat_delimiters e = function
+  | None -> e
+  | Some sc -> CPatDelimiters (dummy_loc,sc,e)
+
+(**********************************************************************)
+(* conversion of references                                           *)
+
+let ids_of_ctxt ctxt =
+  Array.to_list
+    (Array.map
+       (function c -> match kind_of_term c with
+	  | Var id -> id
+	  | _ ->
+       error
+       "Termast: arbitrary substitution of references not yet implemented")
+     ctxt)
+
+let idopt_of_name = function 
+  | Name id -> Some id
+  | Anonymous -> None
+
+let extern_evar loc n =
+(*
+  msgerrnl (str 
+    "Warning: existential variable turned into meta-variable during externalization");
+  CPatVar (loc,(false,make_ident "META" (Some n)))
+*)
+  CEvar (loc,n)
+
+let raw_string_of_ref = function
+  | ConstRef kn -> 
+      "CONST("^(string_of_kn kn)^")"
+  | IndRef (kn,i) ->
+      "IND("^(string_of_kn kn)^","^(string_of_int i)^")"
+  | ConstructRef ((kn,i),j) -> 
+      "CONSTRUCT("^
+      (string_of_kn kn)^","^(string_of_int i)^","^(string_of_int j)^")"
+  | VarRef id -> 
+      "SECVAR("^(string_of_id id)^")"
+
+(* v7->v8 translation *)
+
+let name_app f = function
+  | Name id -> Name (f id)
+  | Anonymous -> Anonymous
+
+let rec translate_ident_string = function
+    (* translate keyword *)
+  | ("at" | "IF" | "forall" | "fun" | "match" | "fix" | "cofix" | "for" | "let"
+    | "if"  | "then" | "else" | "return" | "mod" | "where" 
+    | "exists" | "exists2" | "using" as s) ->
+      let s' = s^"_" in
+      msgerrnl
+      (str ("Warning: '"^
+          s^"' is now a keyword; it has been translated to '"^s'^"'"));
+      s'
+(* Le conflit est en fait surtout avec Eval dans Definition et c'est gere dans
+   Ppconstrnew
+  | "eval" as s ->
+      let s' = s^"_" in
+      msgerrnl
+      (str ("Warning: '"^
+          s^"' is a conflicting ident; it has been translated to '"^s'^"'"));
+      s'
+*)
+
+  (* avoid _ *)
+  | "_" -> 
+      msgerrnl (str 
+        "Warning: '_' is no longer an ident; it has been translated to 'x_'");
+      "x_"
+  (* avoid @ *)
+  | s when String.contains s '@' ->
+      let n = String.index s '@' in 
+      translate_ident_string
+      (String.sub s 0 n ^ "'at'" ^ String.sub s (n+1) (String.length s -n-1))
+  | s -> s
+
+let translate_ident id =
+  id_of_string (translate_ident_string (string_of_id id))
+
+let is_coq_root d =
+  let d = repr_dirpath d in d <> [] & string_of_id (list_last d) = "Coq"
+
+let is_dir dir s =
+  let d = repr_dirpath dir in
+  d <> [] & string_of_id (List.hd d) = s
+
+let is_module m = is_dir (Lib.library_dp()) m
+
+let bp = ["BinPos"]
+let bz = ["BinInt"]
+let bn = ["BinNat"]
+let pn = ["nat"]
+let zc = ["Zcompare"]
+let lo = ["Logic"]
+let da = ["Datatypes"]
+let zabs = ["Zabs"]
+let zo = ["Zorder"]
+let zn = ["Znat"]
+let wz = ["Wf_Z"]
+let mu = ["Mult"]
+let pl = ["Plus"]
+let mi = ["Minus"]
+let le = ["Le"]
+let gt = ["Gt"]
+let lt = ["Lt"]
+let be = ["Between"]
+let bo = ["Bool"]
+let c dir = 
+  let d = repr_dirpath dir in
+  if d = [] then [] else [string_of_id (List.hd d)]
+
+let translation_table = [
+  (* ZArith *)
+"double_moins_un", (bp,"Pdouble_minus_one");
+"double_moins_deux", (bp,"Pdouble_minus_two");
+"is_double_moins_un", (bp,"Psucc_o_double_minus_one_eq_xO");
+"double_moins_un_add_un_xI", (bp,"Pdouble_minus_one_o_succ_eq_xI");
+"add_un_Zs", (bz,"Zpos_succ_morphism");
+"entier", (bn,"N");
+"entier_of_Z", (bz,"Zabs_N");
+"Z_of_entier", (bz,"Z_of_N");
+"SUPERIEUR", (da,"Gt");
+"EGAL", (da,"Eq");
+"INFERIEUR", (da,"Lt");
+"add", (bp,"Pplus");
+"add_carry", (bp,"Pplus_carry");
+"add_assoc", (bp,"Pplus_assoc");
+"add_sym", (bp,"Pplus_comm");
+"add_x_x", (bp,"Pplus_diag");
+"add_carry_add", (bp,"Pplus_carry_plus");
+"simpl_add_r", (bp,"Pplus_reg_r");
+"simpl_add_l", (bp,"Pplus_reg_l");
+"simpl_add_carry_r", (bp,"Pplus_carry_reg_r");
+"simpl_add_carry_l", (bp,"Pplus_carry_reg_l");
+"simpl_times_r", (bp,"Pmult_reg_r");
+"simpl_times_l", (bp,"Pmult_reg_l");
+(*
+"xO_xI_add_double_moins_un", (bp,"xO_xI_plus_double_minus_one");
+*)
+"double_moins_un_plus_xO_double_moins_un",
+  (bp,"Pdouble_minus_one_plus_xO_double_minus_one");
+"add_xI_double_moins_un", (bp,"Pplus_xI_double_minus_one");
+"add_xO_double_moins_un", (bp,"Pplus_xO_double_minus_one");
+"iter_pos_add", (bp,"iter_pos_plus");
+"add_no_neutral", (bp,"Pplus_no_neutral");
+"add_carry_not_add_un", (bp,"Pplus_carry_no_neutral");
+"times_add_distr", (bp,"Pmult_plus_distr_l");
+"times_add_distr_l", (bp,"Pmult_plus_distr_r");
+"times_true_sub_distr", (bp,"Pmult_minus_distr_l");
+"times_sym", (bp,"Pmult_comm");
+"times_assoc", (bp,"Pmult_assoc");
+"times_convert", (bp,"nat_of_P_mult_morphism");
+"true_sub", (bp,"Pminus");
+"times_x_1", (bp,"Pmult_1_r");
+"times_x_double", (bp,"Pmult_xO_permute_r"); 
+   (* Changer en Pmult_xO_distrib_r_reverse *)
+"times_x_double_plus_one", (bp,"Pmult_xI_permute_r"); (* Changer ? *)
+"times_discr_xO_xI", (bp,"Pmult_xI_mult_xO_discr");
+"times_discr_xO", (bp,"Pmult_xO_discr");
+"times_one_inversion_l", (bp,"Pmult_1_inversion_l");
+"true_sub_convert", (bp,"nat_of_P_minus_morphism");
+"compare_true_sub_right", (bp,"Pcompare_minus_r");
+"compare_true_sub_left", (bp,"Pcompare_minus_l");
+"sub_add", (bp,"Pplus_minus" (* similar to le_plus_minus in Arith *));
+"sub_add_one", (bp,"Ppred_succ");
+"add_sub_one", (bp,"Psucc_pred");
+"add_un", (bp,"Psucc");
+"add_un_discr", (bp,"Psucc_discr");
+"add_un_not_un", (bp,"Psucc_not_one");
+"add_un_inj", (bp,"Psucc_inj");
+"xI_add_un_xO", (bp,"xI_succ_xO");
+"ZL12", (bp,"Pplus_one_succ_r");
+"ZL12bis", (bp,"Pplus_one_succ_l");
+"ZL13", (bp,"Pplus_carry_spec");
+      (* Changer en Pplus_succ_distrib_r_reverse ? *)
+"ZL14", (bp,"Pplus_succ_permute_r");
+      (* Changer en Plus_succ_distrib_l_reverse *)
+"ZL14bis", (bp,"Pplus_succ_permute_l");
+"sub_un", (bp,"Ppred");
+"sub_pos", (bp,"Pminus_mask");
+"sub_pos_x_x", (bp,"Pminus_mask_diag");
+(*"sub_pos_x_x", (bp,"Pminus_mask_diag");*)
+"sub_pos_SUPERIEUR", (bp,"Pminus_mask_Gt");
+"sub_neg", (bp,"Pminus_mask_carry");
+"Zdiv2_pos", (bp,"Pdiv2");
+"Pdiv2", (["Zbinary"],"Zdiv2_ge_compat");
+"ZERO", (bz,"Z0");
+"POS", (bz,"Zpos");
+"NEG", (bz,"Zneg");
+"Nul", (bn,"N0");
+"Pos", (bn,"Npos");
+"Un_suivi_de", (bn,"Ndouble_plus_one");
+"Zero_suivi_de", (bn,"Ndouble");
+"Un_suivi_de_mask", (bp,"Pdouble_plus_one_mask");
+"Zero_suivi_de_mask", (bp,"Pdouble_mask");
+"ZS", (bp,"double_eq_zero_inversion");
+"US", (bp,"double_plus_one_zero_discr");
+"USH", (bp,"double_plus_one_eq_one_inversion");
+"ZSH", (bp,"double_eq_one_discr");
+"ZPminus_add_un_permute", (bz,"ZPminus_succ_permute");
+"ZPminus_add_un_permute_Zopp", (bz,"ZPminus_succ_permute_opp");
+"ZPminus_double_moins_un_xO_add_un", (bz,"ZPminus_double_minus_one_xO_succ");
+"ZL1", (bp,"xO_succ_permute");  (* ?? *)
+"Zplus_assoc_r", (bz,"Zplus_assoc_reverse");
+"Zplus_sym", (bz,"Zplus_comm");
+"Zero_left", (bz,"Zplus_0_l");
+"Zero_right", (bz,"Zplus_0_r");
+"Zplus_n_O", (bz,"Zplus_0_r_reverse");
+"Zplus_unit_left", (bz,"Zplus_0_simpl_l");
+"Zplus_unit_right", (bz,"Zplus_0_simpl_l_reverse");
+"Zplus_Zopp_expand", (bz,"Zplus_opp_expand");
+"Zn_Sn", (bz,"Zsucc_discr");
+"Zs", (bz,"Zsucc");
+"Psucc_Zs", (bz,"Zpos_succ_permute");
+"Zs_pred", (bz,"Zsucc_pred");
+"Zpred_Sn", (bz,"Zpred_succ");
+"Zminus_n_O", (bz,"Zminus_0_l_reverse");
+"Zminus_n_n", (bz,"Zminus_diag_reverse");
+"Zminus_Sn_m", (bz,"Zminus_succ_l");
+"Zeq_Zminus", (bz,"Zeq_minus");
+"Zminus_Zeq", (bz,"Zminus_eq");
+"Zplus_minus", (bz,"Zplus_minus_eq");
+"Zminus_plus", (bz,"Zminus_plus");
+"Zminus_plus_simpl", (bz,"Zminus_plus_simpl_l_reverse");
+"Zminus_Zplus_compatible", (bz,"Zminus_plus_simpl_r");
+"Zle_plus_minus", (bz,"Zplus_minus");
+"Zopp_Zplus", (bz,"Zopp_plus_distr");
+"Zopp_Zopp", (bz,"Zopp_involutive");
+"Zopp_NEG", (bz,"Zopp_neg");
+"Zopp_Zdouble", (bz,"Zopp_double");
+"Zopp_Zdouble_plus_one", (bz,"Zopp_double_plus_one");
+"Zopp_Zdouble_minus_one", (bz,"Zopp_double_minus_one");
+"Zplus_inverse_r", (bz,"Zplus_opp_r");
+"Zplus_inverse_l", (bz,"Zplus_opp_l");
+"Zplus_S_n", (bz,"Zplus_succ_l");
+"Zplus_n_Sm", (bz,"Zplus_succ_r");
+"Zplus_Snm_nSm", (bz,"Zplus_succ_comm");
+"Zmult_assoc_r", (bz,"Zmult_assoc_reverse");
+"Zmult_sym", (bz,"Zmult_comm");
+"Zmult_eq", (bz,"Zmult_integral_l");
+"Zmult_zero", (bz,"Zmult_integral");
+"Zero_mult_left", (bz,"Zmult_0_l");
+"Zero_mult_right", (bz,"Zmult_0_r");
+"Zmult_1_n", (bz,"Zmult_1_l");
+"Zmult_n_1", (bz,"Zmult_1_r");
+"Zmult_n_O", (bz,"Zmult_0_r_reverse");
+"Zopp_one", (bz,"Zopp_eq_mult_neg_1");
+"Zopp_Zmult", (bz,"Zopp_mult_distr_l_reverse");
+"Zopp_Zmult_r", (bz,"Zopp_mult_distr_r");
+"Zopp_Zmult_l", (bz,"Zopp_mult_distr_l");
+"Zmult_Zopp_Zopp", (bz,"Zmult_opp_opp");
+"Zmult_Zopp_left", (bz,"Zmult_opp_comm");
+"Zmult_Zplus_distr", (bz,"Zmult_plus_distr_r");
+"Zmult_plus_distr", (bz,"Zmult_plus_distr_r");
+"Zmult_Zminus_distr_r", (bz,"Zmult_minus_distr_l");
+"Zmult_Zminus_distr_l", (bz,"Zmult_minus_distr_r");
+"Zcompare_Zplus_compatible", (zc,"Zcompare_plus_compat");
+"Zcompare_Zplus_compatible2", (zc,"Zplus_compare_compat");
+"Zcompare_Zmult_compatible", (zc,"Zcompare_mult_compat");
+"inject_nat", (bz,"Z_of_nat");
+"inject_nat_complete", (wz,"Z_of_nat_complete");
+"inject_nat_complete_inf", (wz,"Z_of_nat_complete_inf");
+"inject_nat_prop", (wz,"Z_of_nat_prop");
+"inject_nat_set", (wz,"Z_of_nat_set");
+"convert", (bp,"nat_of_P");
+"anti_convert", (bp,"P_of_succ_nat");
+"positive_to_nat", (bp,"Pmult_nat");
+"Zopp_intro", (bz,"Zopp_inj");
+"plus_iter_add", (bp,"plus_iter_eq_plus");
+"compare", (bp,"Pcompare");
+"iter_convert", (["Zmisc"],"iter_nat_of_P");
+"ZLSI", (bp,"Pcompare_Gt_Lt");
+"ZLIS", (bp,"Pcompare_Lt_Gt");
+"ZLII", (bp,"Pcompare_Lt_Lt");
+"ZLSS", (bp,"Pcompare_Gt_Gt");
+  (* Pnat *)
+"convert_intro", (pn,"nat_of_P_inj");
+"convert_add", (pn,"nat_of_P_plus_morphism");
+"convert_add_un", (pn,"Pmult_nat_succ_morphism");
+"cvt_add_un", (pn,"nat_of_P_succ_morphism");
+"convert_add_carry", (pn,"Pmult_nat_plus_carry_morphism");
+"compare_convert_O", (pn,"lt_O_nat_of_P");
+"add_verif", (pn,"Pmult_nat_l_plus_morphism");
+"ZL2", (pn,"Pmult_nat_r_plus_morphism");
+"compare_positive_to_nat_O", (pn,"le_Pmult_nat");
+(* Trop spécifique ?
+"ZL6", (pn,"Pmult_nat_plus_shift_morphism");
+*)
+"ZL15", (pn,"Pplus_carry_pred_eq_plus");
+"cvt_carry", (pn,"nat_of_P_plus_carry_morphism");
+"compare_convert1", (pn,"Pcompare_not_Eq");
+"compare_convert_INFERIEUR", (pn,"nat_of_P_lt_Lt_compare_morphism");
+"compare_convert_SUPERIEUR", (pn,"nat_of_P_gt_Gt_compare_morphism");
+"compare_convert_EGAL", (pn,"Pcompare_Eq_eq");
+"convert_compare_INFERIEUR", (pn,"nat_of_P_lt_Lt_compare_complement_morphism");
+"convert_compare_SUPERIEUR", (pn,"nat_of_P_gt_Gt_compare_complement_morphism");
+"convert_compare_EGAL", (pn,"Pcompare_refl");
+"bij1", (pn,"nat_of_P_o_P_of_succ_nat_eq_succ");
+"bij2", (pn,"P_of_succ_nat_o_nat_of_P_eq_succ");
+"bij3", (pn,"pred_o_P_of_succ_nat_o_nat_of_P_eq_id");
+  (* Zcompare *)
+"Zcompare_EGAL", (zc,"Zcompare_Eq_iff_eq");
+"Zcompare_EGAL_eq", (zc,"Zcompare_Eq_eq");
+"Zcompare_x_x", (zc,"Zcompare_refl");
+"Zcompare_et_un", (zc,"Zcompare_Gt_not_Lt");
+"Zcompare_trans_SUPERIEUR", (zc,"Zcompare_Gt_trans");
+"Zcompare_n_S", (zc,"Zcompare_succ_compat");
+"SUPERIEUR_POS", (zc,"Zcompare_Gt_spec");
+"Zcompare_ANTISYM", (zc,"Zcompare_Gt_Lt_antisym");
+"Zcompare_Zs_SUPERIEUR", (zc,"Zcompare_succ_Gt");
+"Zcompare_Zopp", (zc,"Zcompare_opp");
+"POS_inject", (zn,"Zpos_eq_Z_of_nat_o_nat_of_P");
+"absolu", (bz,"Zabs_nat");
+"absolu_lt", (zabs,"Zabs_nat_lt" (* "Zabs_nat_lt_morphism_pos" ? *));
+"Zeq_add_S", (bz,"Zsucc_inj");
+"Znot_eq_S", (bz,"Zsucc_inj_contrapositive");
+"Zeq_S", (bz,"Zsucc_eq_compat");
+"Zsimpl_plus_l", (bz,"Zplus_reg_l");
+"Zplus_simpl", (bz,"Zplus_eq_compat");
+"POS_gt_ZERO", (zo,"Zgt_pos_0");
+"ZERO_le_POS", (zo,"Zle_0_pos");
+"ZERO_le_inj", (zo,"Zle_0_nat");
+"NEG_lt_ZERO", (zo,"Zlt_neg_0");
+"Zlt_ZERO_pred_le_ZERO", (zo,"Zlt_0_le_0_pred");
+"POS_xI", (bz,"Zpos_xI");
+"POS_xO", (bz,"Zpos_xO");
+"NEG_xI", (bz,"Zneg_xI");
+"NEG_xO", (bz,"Zneg_xO");
+"POS_add", (bz,"Zpos_plus_distr");
+"NEG_add", (bz,"Zneg_plus_distr");
+  (* Z Orders *)
+"not_Zge", (zo,"Znot_ge_lt");
+"not_Zlt", (zo,"Znot_lt_ge");
+"not_Zle", (zo,"Znot_le_gt");
+"not_Zgt", (zo,"Znot_gt_le");
+"Zgt_not_sym", (zo,"Zgt_asym");
+"Zlt_not_sym", (zo,"Zlt_asym");
+"Zlt_n_n", (zo,"Zlt_irrefl");
+"Zgt_antirefl", (zo,"Zgt_irrefl");
+"Zgt_reg_l", (zo,"Zplus_gt_compat_l");
+"Zgt_reg_r", (zo,"Zplus_gt_compat_r");
+"Zlt_reg_l", (zo,"Zplus_lt_compat_l");
+"Zlt_reg_r", (zo,"Zplus_lt_compat_r");
+"Zle_reg_l", (zo,"Zplus_le_compat_l");
+"Zle_reg_r", (zo,"Zplus_le_compat_r");
+"Zlt_le_reg", (zo,"Zplus_lt_le_compat");
+"Zle_lt_reg", (zo,"Zplus_le_lt_compat");
+"Zle_plus_plus", (zo,"Zplus_le_compat");
+"Zlt_Zplus", (zo,"Zplus_lt_compat");
+"Zle_O_plus", (zo,"Zplus_le_0_compat");
+"Zle_mult_simpl", (zo,"Zmult_le_reg_r");
+"Zge_mult_simpl", (zo,"Zmult_ge_reg_r");
+"Zgt_mult_simpl", (zo,"Zmult_gt_reg_r");
+"Zsimpl_gt_plus_l", (zo,"Zplus_gt_reg_l");
+"Zsimpl_gt_plus_r", (zo,"Zplus_gt_reg_r");
+"Zsimpl_le_plus_l", (zo,"Zplus_le_reg_l");
+"Zsimpl_le_plus_r", (zo,"Zplus_le_reg_r");
+"Zsimpl_lt_plus_l", (zo,"Zplus_lt_reg_l");
+"Zsimpl_lt_plus_r", (zo,"Zplus_lt_reg_r");
+"Zlt_Zmult_right2", (zo,"Zmult_gt_0_lt_reg_r");
+"Zlt_Zmult_right", (zo,"Zmult_gt_0_lt_compat_r");
+"Zle_Zmult_right2", (zo,"Zmult_gt_0_le_reg_r");
+"Zle_Zmult_right", (zo,"Zmult_gt_0_le_compat_r");
+"Zgt_Zmult_right", (zo,"Zmult_gt_compat_r");
+"Zgt_Zmult_left", (zo,"Zmult_gt_compat_l");
+"Zlt_Zmult_left", (zo,"Zmult_gt_0_lt_compat_l");
+"Zcompare_Zmult_right", (zc,"Zmult_compare_compat_r");
+"Zcompare_Zmult_left", (zc,"Zmult_compare_compat_l");
+"Zplus_Zmult_2", (bz,"Zplus_diag_eq_mult_2");
+"Zmult_Sm_n", (bz,"Zmult_succ_l_reverse");
+"Zmult_n_Sm", (bz,"Zmult_succ_r_reverse");
+"Zmult_le", (zo,"Zmult_le_0_reg_r");
+"Zmult_reg_left", (bz,"Zmult_reg_l");
+"Zmult_reg_right", (bz,"Zmult_reg_r");
+"Zle_ZERO_mult", (zo,"Zmult_le_0_compat");
+"Zgt_ZERO_mult", (zo,"Zmult_gt_0_compat");
+"Zle_mult", (zo,"Zmult_gt_0_le_0_compat");
+"Zmult_lt", (zo,"Zmult_gt_0_lt_0_reg_r");
+"Zmult_gt", (zo,"Zmult_gt_0_reg_l");
+"Zle_Zmult_pos_right", (zo,"Zmult_le_compat_r");
+"Zle_Zmult_pos_left", (zo,"Zmult_le_compat_l");
+"Zge_Zmult_pos_right", (zo,"Zmult_ge_compat_r");
+"Zge_Zmult_pos_left", (zo,"Zmult_ge_compat_l");
+"Zge_Zmult_pos_compat", (zo,"Zmult_ge_compat");
+"Zlt_Zcompare", (zo,"Zlt_compare");
+"Zle_Zcompare", (zo,"Zle_compare");
+"Zgt_Zcompare", (zo,"Zgt_compare");
+"Zge_Zcompare", (zo,"Zge_compare");
+  (* ex-IntMap *)
+"convert_xH", (pn,"nat_of_P_xH");
+"convert_xO", (pn,"nat_of_P_xO");
+"convert_xI", (pn,"nat_of_P_xI");
+"positive_to_nat_mult", (pn,"Pmult_nat_mult_permute");
+"positive_to_nat_2", (pn,"Pmult_nat_2_mult_2_permute");
+"positive_to_nat_4", (pn,"Pmult_nat_4_mult_2_permute");
+  (* ZArith and Arith orders *)
+"Zle_refl", (zo,"Zeq_le");
+"Zle_n", (zo,"Zle_refl");
+"Zle_trans_S", (zo,"Zle_succ_le");
+"Zgt_trans_S", (zo,"Zge_trans_succ");
+"Zgt_S", (zo,"Zgt_succ_gt_or_eq");
+"Zle_Sn_n", (zo,"Znot_le_succ");
+"Zlt_n_Sn", (zo,"Zlt_succ");
+"Zlt_S", (zo,"Zlt_lt_succ");
+"Zlt_n_S", (zo,"Zsucc_lt_compat");
+"Zle_n_S", (zo,"Zsucc_le_compat");
+"Zgt_n_S", (zo,"Zsucc_gt_compat");
+"Zlt_S_n", (zo,"Zsucc_lt_reg");
+"Zgt_S_n", (zo,"Zsucc_gt_reg");
+"Zle_S_n", (zo,"Zsucc_le_reg");
+"Zle_0_plus", (zo,"Zplus_le_0_compat");
+"Zgt_Sn_n", (zo,"Zgt_succ");
+"Zgt_le_S", (zo,"Zgt_le_succ");
+"Zgt_S_le", (zo,"Zgt_succ_le");
+"Zle_S_gt", (zo,"Zlt_succ_gt");
+"Zle_gt_S", (zo,"Zlt_gt_succ");
+"Zgt_pred", (zo,"Zgt_succ_pred");
+"Zlt_pred", (zo,"Zlt_succ_pred");
+"Zgt0_le_pred", (zo,"Zgt_0_le_0_pred");
+"Z_O_1", (zo,"Zlt_0_1");
+"Zle_NEG_POS", (zo,"Zle_neg_pos");
+"Zle_n_Sn", (zo,"Zle_succ");
+"Zle_pred_n", (zo,"Zle_pred");
+"Zlt_pred_n_n", (zo,"Zlt_pred");
+"Zlt_le_S", (zo,"Zlt_le_succ");
+"Zlt_n_Sm_le", (zo,"Zlt_succ_le");
+"Zle_lt_n_Sm", (zo,"Zle_lt_succ");
+"Zle_le_S", (zo,"Zle_le_succ");
+"Zlt_minus", (zo,"Zlt_minus_simpl_swap");
+"le_trans_S", (le,"le_Sn_le");
+(* Znumtheory *)
+"Zdivide_Zmod", ([],"Zdivide_mod");
+"Zmod_Zdivide", ([],"Zmod_divide");
+"Zdivide_mult_left", ([],"Zmult_divide_compat_l");
+"Zdivide_mult_right", ([],"Zmult_divide_compat_r");
+"Zdivide_opp", ([],"Zdivide_opp_r");
+"Zdivide_opp_rev", ([],"Zdivide_opp_r_rev");
+"Zdivide_opp_left", ([],"Zdivide_opp_l");
+"Zdivide_opp_left_rev", ([],"Zdivide_opp_l_rev");
+"Zdivide_right", ([],"Zdivide_mult_r");
+"Zdivide_left", ([],"Zdivide_mult_l");
+"Zdivide_plus", ([],"Zdivide_plus_r");
+"Zdivide_minus", ([],"Zdivide_minus_l");
+"Zdivide_a_ab", ([],"Zdivide_factor_r");
+"Zdivide_a_ba", ([],"Zdivide_factor_l");
+(* Arith *)
+(* Peano.v
+"plus_n_O", ("plus_0_r_reverse");
+"plus_O_n", ("plus_0_l");
+*)
+"plus_assoc_l", (pl,"plus_assoc");
+"plus_assoc_r", (pl,"plus_assoc_reverse");
+"plus_sym", (pl,"plus_comm");
+"mult_sym", (mu,"mult_comm");
+"max_sym", (["Max"],"max_comm");
+"min_sym", (["Min"],"min_comm");
+"gt_not_sym", (gt,"gt_asym");
+"lt_not_sym", (lt,"lt_asym");
+"gt_antirefl", (gt,"gt_irrefl");
+"lt_n_n", (lt,"lt_irrefl");
+(* Trop utilisé dans CoqBook | "le_n" -> "le_refl"*)
+"simpl_plus_l", (pl,"plus_reg_l");
+"simpl_plus_r", (pl,"plus_reg_r");
+"fact_growing", (["Factorial"],"fact_le");
+"mult_assoc_l", (mu,"mult_assoc");
+"mult_assoc_r", (mu,"mult_assoc_reverse");
+"mult_plus_distr", (mu,"mult_plus_distr_r");
+"mult_plus_distr_r", (mu,"mult_plus_distr_l");
+"mult_minus_distr", (mu,"mult_minus_distr_r");
+"mult_1_n", (mu,"mult_1_l");
+"mult_n_1", (mu,"mult_1_r");
+(* Peano.v
+"mult_n_O", ("mult_O_r_reverse");
+"mult_n_Sm", ("mult_S_r_reverse");
+*)
+"mult_le", (mu,"mult_le_compat_l");
+"le_mult_right", (mu,"mult_le_compat_r");
+"le_mult_mult", (mu,"mult_le_compat");
+"mult_lt", (mu,"mult_S_lt_compat_l");
+"lt_mult_right", (mu,"mult_lt_compat_r");
+"mult_le_conv_1", (mu,"mult_S_le_reg_l");
+"exists", (be,"exists_between");
+"IHexists", ([],"IHexists_between");
+(* Peano.v
+"pred_Sn", ("pred_S");
+*)
+"inj_minus_aux", (mi,"not_le_minus_0");
+"minus_x_x", (mi,"minus_diag");
+"minus_plus_simpl", (mi,"minus_plus_simpl_l_reverse");
+"gt_reg_l", (gt,"plus_gt_compat_l");
+"le_reg_l", (pl,"plus_le_compat_l");
+"le_reg_r", (pl,"plus_le_compat_r");
+"lt_reg_l", (pl,"plus_lt_compat_l");
+"lt_reg_r", (pl,"plus_lt_compat_r");
+"le_plus_plus", (pl,"plus_le_compat");
+"le_lt_plus_plus", (pl,"plus_le_lt_compat");
+"lt_le_plus_plus", (pl,"plus_lt_le_compat");
+"lt_plus_plus", (pl,"plus_lt_compat");
+"plus_simpl_l", (pl,"plus_reg_l");
+"simpl_gt_plus_l", (pl,"plus_gt_reg_l");
+"simpl_le_plus_l", (pl,"plus_le_reg_l");
+"simpl_lt_plus_l", (pl,"plus_lt_reg_l");
+(* Noms sur le principe de ceux de Z
+"le_n_S", ("S_le_compat");
+"le_n_Sn", ("le_S");
+(*"le_O_n", ("??" *));
+"le_pred_n", ("le_pred");
+"le_trans_S", ("le_S_le");
+"le_S_n", ("S_le_reg");
+"le_Sn_O", ("not_le_S_O");
+"le_Sn_n", ("not_le_S");
+*)
+  (* Init *)
+"IF", (lo,"IF_then_else");
+  (* Lists *)
+"idempot_rev", (["List"],"rev_involutive");
+"forall", (["Streams"],"HereAndFurther");
+  (* Bool *)
+"orb_sym", (bo,"orb_comm");
+"andb_sym", (bo,"andb_comm");
+  (* Ring *)
+"SR_plus_sym", (["Ring_theory"],"SR_plus_comm");
+"SR_mult_sym", (["Ring_theory"],"SR_mult_comm");
+"Th_plus_sym", (["Ring_theory"],"Th_plus_comm");
+"Th_mul_sym", (["Ring_theory"],"Th_mult_comm");
+"SSR_plus_sym", (["Setoid_ring_theory"],"SSR_plus_comm");
+"SSR_mult_sym", (["Setoid_ring_theory"],"SSR_mult_comm");
+"STh_plus_sym", (["Setoid_ring_theory"],"STh_plus_comm");
+"STh_mul_sym", (["Setoid_ring_theory"],"STh_mult_comm");
+  (* Reals *)
+(*
+"Rabsolu", ("Rabs");
+"Rabsolu_pos_lt", ("Rabs_pos_lt");
+"Rabsolu_no_R0", ("Rabs_no_R0");
+"Rabsolu_Rabsolu", ("Rabs_Rabs");
+"Rabsolu_mult", ("Rabs_mult");
+"Rabsolu_triang", ("Rabs_triang");
+"Rabsolu_Ropp", ("Rabs_Ropp");
+"Rabsolu_right", ("Rabs_right");
+...
+"case_Rabsolu", ("case_Rabs");
+"Pow_Rabsolu", ("Pow_Rabs");
+...
+*)
+(* Raxioms *)
+"complet", ([],"completeness");
+"complet_weak", ([],"completeness_weak");
+"Rle_sym1", ([],"Rle_ge");
+"Rmin_sym", ([],"Rmin_comm");
+"Rplus_sym", ([],"Rplus_comm");
+"Rmult_sym", ([],"Rmult_comm");
+"Rsqr_times", ([],"Rsqr_mult");
+"sqrt_times", ([],"sqrt_mult");
+"Rmult_1l", ([],"Rmult_1_l");
+"Rplus_Ol", ([],"Rplus_0_l");
+"Rplus_Ropp_r", ([],"Rplus_opp_r");
+"Rmult_Rplus_distr", ([],"Rmult_plus_distr_l");
+"Rlt_antisym", ([],"Rlt_asym");
+(* RIneq *)
+"Rlt_antirefl", ([],"Rlt_irrefl");
+"Rlt_compatibility", ([],"Rplus_lt_compat_l");
+"Rgt_plus_plus_r", ([],"Rplus_gt_compat_l");
+"Rgt_r_plus_plus", ([],"Rplus_gt_reg_l");
+"Rge_plus_plus_r", ([],"Rplus_ge_compat_l");
+"Rge_r_plus_plus", ([],"Rplus_ge_reg_l");
+(* Si on en change un, il faut changer tous les autres R*_monotony *)
+"Rlt_monotony", ([],"Rmult_lt_compat_l");
+"Rlt_monotony_r", ([],"Rmult_lt_compat_r");
+"Rlt_monotony_contra", ([],"Rmult_lt_reg_l");
+(*"Rlt_monotony_rev", ([],"Rmult_lt_reg_l");*)
+"Rlt_anti_monotony", ([],"Rmult_lt_gt_compat_neg_l");
+"Rle_monotony", ([],"Rmult_le_compat_l");
+"Rle_monotony_r", ([],"Rmult_le_compat_r");
+"Rle_monotony_contra", ([],"Rmult_le_reg_l");
+"Rle_anti_monotony1", ([],"Rmult_le_compat_neg_l");
+"Rle_anti_monotony", ([],"Rmult_le_ge_compat_neg_l");
+"Rge_monotony", ([],"Rmult_ge_compat_r");
+"Rge_ge_eq", ([],"Rge_antisym");
+(* Le reste de RIneq *)
+"imp_not_Req", ([],"Rlt_dichotomy_converse");
+"Req_EM", ([],"Req_dec");
+"total_order", ([],"Rtotal_order");
+"not_Req", ([],"Rdichotomy");
+(* "Rlt_le" -> c dir,"Rlt_le_weak" ? *)
+"not_Rle", ([],"Rnot_le_lt");
+"not_Rge", ([],"Rnot_ge_lt");
+"Rlt_le_not", ([],"Rlt_not_le");
+"Rle_not", ([],"Rgt_not_le");
+"Rle_not_lt", ([],"Rle_not_lt");
+"Rlt_ge_not", ([],"Rlt_not_ge");
+"eq_Rle", ([],"Req_le");
+"eq_Rge", ([],"Req_ge");
+"eq_Rle_sym", ([],"Req_le_sym");
+"eq_Rge_sym", ([],"Req_ge_sym");
+(* "Rle_le_eq" -> ?   x<=y/\y<=x <-> x=y *)
+"Rlt_rew", ([],"Rlt_eq_compat");
+"total_order_Rlt", ([],"Rlt_dec");
+"total_order_Rle", ([],"Rle_dec");
+"total_order_Rgt", ([],"Rgt_dec");
+"total_order_Rge", ([],"Rge_dec");
+"total_order_Rlt_Rle", ([],"Rlt_le_dec");
+(* "Rle_or_lt" -> c dir,"Rle_or_lt"*)
+"total_order_Rle_Rlt_eq", ([],"Rle_lt_or_eq_dec");
+(* "inser_trans_R" -> c dir,"Rle_lt_inser_trans" ?*)
+(* "Rplus_ne" -> c dir,"Rplus_0_r_l" ? *)
+"Rplus_Or", ([],"Rplus_0_r");
+"Rplus_Ropp_l", ([],"Rplus_opp_l");
+"Rplus_Ropp", ([],"Rplus_opp_r_uniq");
+"Rplus_plus_r", ([],"Rplus_eq_compat_l");
+"r_Rplus_plus", ([],"Rplus_eq_reg_l");
+"Rplus_ne_i", ([],"Rplus_0_r_uniq");
+"Rmult_Or", ([],"Rmult_0_r");
+"Rmult_Ol", ([],"Rmult_0_l");
+(* "Rmult_ne" -> c dir,"Rmult_1_l_r" ? *)
+"Rmult_1r", ([],"Rmult_1_r");
+"Rmult_mult_r", ([],"Rmult_eq_compat_l");
+"r_Rmult_mult", ([],"Rmult_eq_reg_l");
+"without_div_Od", ([],"Rmult_integral");
+"without_div_Oi", ([],"Rmult_eq_0_compat");
+"without_div_Oi1", ([],"Rmult_eq_0_compat_r");
+"without_div_Oi2", ([],"Rmult_eq_0_compat_l");
+"without_div_O_contr", ([],"Rmult_neq_0_reg");
+"mult_non_zero", ([],"Rmult_integral_contrapositive");
+"Rmult_Rplus_distrl", ([],"Rmult_plus_distr_r");
+"Rsqr_O", ([],"Rsqr_0");
+"Rsqr_r_R0", ([],"Rsqr_0_uniq");
+"eq_Ropp", ([],"Ropp_eq_compat");
+"Ropp_O", ([],"Ropp_0");
+"eq_RoppO", ([],"Ropp_eq_0_compat");
+"Ropp_Ropp", ([],"Ropp_involutive");
+"Ropp_neq", ([],"Ropp_neq_0_compat");
+"Ropp_distr1", ([],"Ropp_plus_distr");
+"Ropp_mul1", ([],"Ropp_mult_distr_l_reverse");
+"Ropp_mul2", ([],"Rmult_opp_opp");
+"Ropp_mul3", ([],"Ropp_mult_distr_r_reverse");
+"minus_R0", ([],"Rminus_0_r");
+"Rminus_Ropp", ([],"Rminus_0_l");
+"Ropp_distr2", ([],"Ropp_minus_distr");
+"Ropp_distr3", ([],"Ropp_minus_distr'");
+"eq_Rminus", ([],"Rminus_diag_eq");
+"Rminus_eq", ([],"Rminus_diag_uniq");
+"Rminus_eq_right", ([],"Rminus_diag_uniq_sym");
+"Rplus_Rminus", ([],"Rplus_minus");
+(*
+"Rminus_eq_contra", ([],"Rminus_diag_neq");
+"Rminus_not_eq", ([],"Rminus_neq_diag_sym");
+ "Rminus_not_eq_right" -> ?
+*)
+"Rminus_distr", ([],"Rmult_minus_distr_l");
+"Rinv_R1", ([],"Rinv_1");
+"Rinv_neq_R0", ([],"Rinv_neq_0_compat");
+"Rinv_Rinv", ([],"Rinv_involutive");
+"Rinv_Rmult", ([],"Rinv_mult_distr");
+"Ropp_Rinv", ([],"Ropp_inv_permute");
+(* "Rinv_r_simpl_r" -> OK ? *)
+(* "Rinv_r_simpl_l" -> OK ? *)
+(* "Rinv_r_simpl_m" -> OK ? *)
+"Rinv_Rmult_simpl", ([],"Rinv_mult_simpl"); (* ? *)
+"Rlt_compatibility_r", ([],"Rplus_lt_compat_r");
+"Rlt_anti_compatibility", ([],"Rplus_lt_reg_r");
+"Rle_compatibility", ([],"Rplus_le_compat_l");
+"Rle_compatibility_r", ([],"Rplus_le_compat_r");
+"Rle_anti_compatibility", ([],"Rplus_le_reg_l");
+(* "sum_inequa_Rle_lt" -> ? *)
+"Rplus_lt", ([],"Rplus_lt_compat");
+"Rplus_le", ([],"Rplus_le_compat");
+"Rplus_lt_le_lt", ([],"Rplus_lt_le_compat");
+"Rplus_le_lt_lt", ([],"Rplus_le_lt_compat");
+"Rgt_Ropp", ([],"Ropp_gt_lt_contravar");
+"Rlt_Ropp", ([],"Ropp_lt_gt_contravar");
+"Ropp_Rlt", ([],"Ropp_lt_cancel");  (* ?? *)
+"Rlt_Ropp1", ([],"Ropp_lt_contravar");
+"Rle_Ropp", ([],"Ropp_le_ge_contravar");
+"Ropp_Rle", ([],"Ropp_le_cancel");
+"Rle_Ropp1", ([],"Ropp_le_contravar");
+"Rge_Ropp", ([],"Ropp_ge_le_contravar");
+"Rlt_RO_Ropp", ([],"Ropp_0_lt_gt_contravar");
+"Rgt_RO_Ropp", ([],"Ropp_0_gt_lt_contravar");
+"Rle_RO_Ropp", ([],"Ropp_0_le_ge_contravar");
+"Rge_RO_Ropp", ([],"Ropp_0_ge_le_contravar");
+(* ... cf plus haut pour les lemmes intermediaires *)
+"Rle_Rmult_comp", ([],"Rmult_le_compat");
+   (* Expliciter que la contrainte est r2>0 dans r1<r2 et non 0<r1 ce
+      qui est plus général mais différent de Rmult_le_compat ? *)
+"Rmult_lt", ([],"Rmult_gt_0_lt_compat"); (* Hybride aussi *)
+"Rmult_lt_0", ([],"Rmult_ge_0_gt_0_lt_compat"); (* Un truc hybride *)
+(*
+ "Rlt_minus" -> 
+ "Rle_minus" -> 
+ "Rminus_lt" -> 
+ "Rminus_le" -> 
+ "tech_Rplus" -> 
+*)
+"pos_Rsqr", ([],"Rle_0_sqr");
+"pos_Rsqr1", ([],"Rlt_0_sqr");
+"Rlt_R0_R1", ([],"Rlt_0_1");
+"Rle_R0_R1", ([],"Rle_0_1");
+"Rlt_Rinv", ([],"Rinv_0_lt_compat");
+"Rlt_Rinv2", ([],"Rinv_lt_0_compat");
+"Rinv_lt", ([],"Rinv_lt_contravar");
+"Rlt_Rinv_R1", ([],"Rinv_1_lt_contravar");
+"Rlt_not_ge", ([],"Rnot_lt_ge");
+"Rgt_not_le", ([],"Rnot_gt_le");
+(*
+ "Rgt_ge" -> "Rgt_ge_weak" ?
+*)
+"Rlt_sym", ([],"Rlt_gt_iff");
+(* | "Rle_sym1" -> c dir,"Rle_ge" OK *)
+"Rle_sym2", ([],"Rge_le");
+"Rle_sym", ([],"Rle_ge_iff");
+(*
+ "Rge_gt_trans" -> OK
+ "Rgt_ge_trans" -> OK
+ "Rgt_trans" -> OK
+ "Rge_trans" -> OK
+*)
+"Rgt_RoppO", ([],"Ropp_lt_gt_0_contravar");
+"Rlt_RoppO", ([],"Ropp_gt_lt_0_contravar");
+"Rlt_r_plus_R1", ([],"Rle_lt_0_plus_1");
+"Rlt_r_r_plus_R1", ([],"Rlt_plus_1");
+(* "tech_Rgt_minus" -> ? *)
+(* OK, cf plus haut
+"Rgt_r_plus_plus", ([],"Rplus_gt_reg_l");
+"Rgt_plus_plus_r", ([],"Rplus_gt_compat_l");
+"Rge_plus_plus_r", ([],"Rplus_ge_compat_l");
+"Rge_r_plus_plus", ([],"Rplus_ge_reg_l");
+"Rge_monotony" ->  *)
+(*
+ "Rgt_minus" -> 
+ "minus_Rgt" -> 
+ "Rge_minus" -> 
+ "minus_Rge" -> 
+*)
+"Rmult_gt", ([],"Rmult_gt_0_compat");
+"Rmult_lt_pos", ([],"Rmult_lt_0_compat");  (* lt_0 ou 0_lt ?? *)
+"Rplus_eq_R0_l", ([],"Rplus_eq_0_l"); (* ? *)
+"Rplus_eq_R0", ([],"Rplus_eq_R0");
+"Rplus_Rsr_eq_R0_l", ([],"Rplus_sqr_eq_0_l");
+"Rplus_Rsr_eq_R0", ([],"Rplus_sqr_eq_0");
+(*
+ "S_INR" -> 
+ "S_O_plus_INR" -> 
+ "plus_INR" -> 
+ "minus_INR" -> 
+ "mult_INR" -> 
+ "lt_INR_0" -> 
+ "lt_INR" -> 
+ "INR_lt_1" -> 
+ "INR_pos" -> 
+ "pos_INR" -> 
+ "INR_lt" -> 
+ "le_INR" -> 
+ "not_INR_O" -> 
+ "not_O_INR" -> 
+ "not_nm_INR" -> 
+ "INR_eq" -> 
+ "INR_le" -> 
+ "not_1_INR" -> 
+ "IZN" -> 
+ "INR_IZR_INZ" -> 
+ "plus_IZR_NEG_POS" -> 
+ "plus_IZR" -> 
+ "mult_IZR" -> 
+ "Ropp_Ropp_IZR" -> 
+ "Z_R_minus" -> 
+ "lt_O_IZR" -> 
+ "lt_IZR" -> 
+ "eq_IZR_R0" -> 
+ "eq_IZR" -> 
+ "not_O_IZR" -> 
+ "le_O_IZR" -> 
+ "le_IZR" -> 
+ "le_IZR_R1" -> 
+ "IZR_ge" -> 
+ "IZR_le" -> 
+ "IZR_lt" -> 
+ "one_IZR_lt1" -> 
+ "one_IZR_r_R1" -> 
+ "single_z_r_R1" -> 
+ "tech_single_z_r_R1" -> 
+ "prod_neq_R0" -> 
+ "Rmult_le_pos" -> 
+ "double" -> 
+ "double_var" -> 
+*)
+"gt0_plus_gt0_is_gt0", ([],"Rplus_lt_0_compat");
+"ge0_plus_gt0_is_gt0", ([],"Rplus_le_lt_0_compat");
+"gt0_plus_ge0_is_gt0", ([],"Rplus_lt_le_0_compat");
+"ge0_plus_ge0_is_ge0", ([],"Rplus_le_le_0_compat");
+(*
+ "plus_le_is_le" -> ?
+ "plus_lt_is_lt" -> ?
+*)
+"Rmult_lt2", ([],"Rmult_le_0_lt_compat");
+(* "Rge_ge_eq" -> c dir,"Rge_antisym" OK *)
+]
+
+let translate_v7_string dir s =
+  try
+    let d,s' = List.assoc s translation_table in
+    (if d=[] then c dir else d),s'
+  with Not_found ->
+  (* Special cases *)
+  match s with
+  (* Init *)
+  | "relation" when is_module "Datatypes" or is_dir dir "Datatypes"
+      -> da,"comparison"
+  | "Op" when is_module "Datatypes" or is_dir dir "Datatypes"
+      -> da,"CompOpp"
+  (* BinPos *)
+  | "times" when not (is_module "Mapfold") -> bp,"Pmult"
+  (* Reals *)
+  | s when String.length s >= 7 & (String.sub s 0 7 = "Rabsolu") ->
+      c dir,
+      "Rabs"^(String.sub s 7 (String.length s - 7))
+  | s when String.length s >= 7 &
+      (String.sub s (String.length s - 7) 7 = "Rabsolu") -> c dir,
+      "R"^(String.sub s 0 (String.length s - 7))^"abs"
+  | s when String.length s >= 7 & 
+      let s' = String.sub s 0 7 in
+      (s' = "unicite" or s' = "unicity") -> c dir,
+      "uniqueness"^(String.sub s 7 (String.length s - 7))
+  | s when String.length s >= 3 &
+      let s' = String.sub s 0 3 in
+      s' = "gcd" -> c dir, "Zis_gcd"^(String.sub s 3 (String.length s - 3))
+  (* Default *)
+  | x -> [],x
+
+
+let id_of_v7_string s =
+  id_of_string (if !Options.v7 then s else snd (translate_v7_string empty_dirpath s))
+
+let v7_to_v8_dir_id dir id =
+  if Options.do_translate() then
+    let s = string_of_id id in
+    let dir',s =
+      if (is_coq_root (Lib.library_dp()) or is_coq_root dir)
+      then translate_v7_string dir s else [], s in
+    dir',id_of_string (translate_ident_string s)
+  else [],id
+
+let v7_to_v8_id id = snd (v7_to_v8_dir_id empty_dirpath id)
+
+let short_names =
+  List.map (fun x -> snd (snd x)) translation_table
+
+let is_new_name s =
+  Options.do_translate () &
+  (List.mem s short_names or
+  s = "comparison" or s = "CompOpp" or s = "Pmult" or
+  (String.length s >= 4 & String.sub s 0 4 = "Rabs") or
+  (String.length s >= 4 & String.sub s (String.length s - 3) 3 = "abs"
+                        & s.[0] = 'R') or
+  (String.length s >= 10 & String.sub s 0 10 = "uniqueness"))
+
+let v7_to_v8_dir fulldir dir =
+  if Options.do_translate () & dir <> empty_dirpath then
+    let update s =
+      let l = List.map string_of_id (repr_dirpath dir) in
+      make_dirpath (List.map id_of_string (s :: List.tl l))
+    in
+    let l = List.map string_of_id (repr_dirpath fulldir) in
+    if l = [ "List"; "Lists"; "Coq" ] then update "MonoList"
+    else if l = [ "PolyList"; "Lists"; "Coq" ] then update "List"
+    else dir
+  else dir
+
+let shortest_qualid_of_v7_global ctx ref =
+  let fulldir,_ = repr_path (sp_of_global ref) in
+  let dir,id = repr_qualid (shortest_qualid_of_global ctx ref) in
+  let dir',id = v7_to_v8_dir_id fulldir id in
+  let dir'' =
+    if dir' = [] then
+      (* A name that is not renamed *)
+      if dir = empty_dirpath & is_new_name (string_of_id id)
+      then 
+        (* An unqualified name that is not renamed but which coincides *)
+        (* with a new name: force qualification unless it is a variable *)
+        if fulldir <> empty_dirpath & not (is_coq_root fulldir)
+        then make_dirpath [List.hd (repr_dirpath fulldir)] 
+        else empty_dirpath
+      else v7_to_v8_dir fulldir dir
+    else
+      (* A stdlib name that has been renamed *)
+      try
+        let d,_ = repr_path (Nametab.full_name_cci (make_short_qualid id)) in
+        if not (is_coq_root d) then 
+          (* The user has defined id, then we qualify the new name *)
+          v7_to_v8_dir fulldir (make_dirpath (List.map id_of_string dir'))
+        else empty_dirpath
+      with Not_found -> v7_to_v8_dir fulldir dir in
+  make_qualid dir'' id
+
+let extern_reference loc vars r =
+  try Qualid (loc,shortest_qualid_of_v7_global vars r)
+  with Not_found ->
+    (* happens in debugger *)
+    Ident (loc,id_of_string (raw_string_of_ref r))
+
+(************************************************************************)
+(* Equality up to location (useful for translator v8) *)
+
+let rec check_same_pattern p1 p2 =
+  match p1, p2 with
+    | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) when i1=i2 ->
+        check_same_pattern a1 a2
+    | CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 ->
+        List.iter2 check_same_pattern a1 a2
+    | CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> ()
+    | CPatNumeral(_,i1), CPatNumeral(_,i2) when i1=i2 -> ()
+    | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 ->
+        check_same_pattern e1 e2
+    | _ -> failwith "not same pattern"
+
+let check_same_ref r1 r2 =
+  match r1,r2 with
+  | Qualid(_,q1), Qualid(_,q2) when q1=q2 -> ()
+  | Ident(_,i1), Ident(_,i2) when i1=i2 -> ()
+  | _ -> failwith "not same ref"
+
+let rec check_same_type ty1 ty2 =
+  match ty1, ty2 with
+  | CRef r1, CRef r2 -> check_same_ref r1 r2
+  | CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 ->
+      List.iter2 (fun (id1,i1,bl1,a1,b1) (id2,i2,bl2,a2,b2) ->
+        if id1<>id2 || i1<>i2 then failwith "not same fix";
+        check_same_fix_binder bl1 bl2;
+        check_same_type a1 a2;
+        check_same_type b1 b2)
+        fl1 fl2
+  | CCoFix(_,(_,id1),fl1), CCoFix(_,(_,id2),fl2) when id1=id2 ->
+      List.iter2 (fun (id1,bl1,a1,b1) (id2,bl2,a2,b2) ->
+        if id1<>id2 then failwith "not same fix";
+        check_same_fix_binder bl1 bl2;
+        check_same_type a1 a2;
+        check_same_type b1 b2)
+        fl1 fl2
+  | CArrow(_,a1,b1), CArrow(_,a2,b2) ->
+      check_same_type a1 a2;
+      check_same_type b1 b2
+  | CProdN(_,bl1,a1), CProdN(_,bl2,a2) ->
+      List.iter2 check_same_binder bl1 bl2;
+      check_same_type a1 a2
+  | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) ->
+      List.iter2 check_same_binder bl1 bl2;
+      check_same_type a1 a2
+  | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when na1=na2 ->
+      check_same_type a1 a2;
+      check_same_type b1 b2
+  | CAppExpl(_,r1,al1), CAppExpl(_,r2,al2) when r1=r2 ->
+      List.iter2 check_same_type al1 al2
+  | CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) ->
+      check_same_type e1 e2;
+      List.iter2 (fun (a1,e1) (a2,e2) ->
+                    if e1<>e2 then failwith "not same expl";
+                    check_same_type a1 a2) al1 al2
+  | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) ->
+      List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2;
+      List.iter2 (fun (_,pl1,r1) (_,pl2,r2) ->
+        List.iter2 check_same_pattern pl1 pl2;
+        check_same_type r1 r2) brl1 brl2
+  | COrderedCase(_,_,_,a1,bl1), COrderedCase(_,_,_,a2,bl2) ->
+      check_same_type a1 a2;
+      List.iter2 check_same_type bl1 bl2
+  | CHole _, CHole _ -> ()
+  | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> ()
+  | CSort(_,s1), CSort(_,s2) when s1=s2 -> ()
+  | CCast(_,a1,b1), CCast(_,a2,b2) ->
+      check_same_type a1 a2;
+      check_same_type b1 b2
+  | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 ->
+      List.iter2 check_same_type e1 e2
+  | CNumeral(_,i1), CNumeral(_,i2) when i1=i2 -> ()
+  | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
+      check_same_type e1 e2
+  | _ when ty1=ty2 -> ()
+  | _ -> failwith "not same type"
+
+and check_same_binder (nal1,e1) (nal2,e2) =
+  List.iter2 (fun (_,na1) (_,na2) ->
+    if na1<>na2 then failwith "not same name") nal1 nal2;
+  check_same_type e1 e2
+
+and check_same_fix_binder bl1 bl2 =
+  List.iter2 (fun b1 b2 ->
+    match b1,b2 with
+        LocalRawAssum(nal1,ty1), LocalRawAssum(nal2,ty2) ->
+          check_same_binder (nal1,ty1) (nal2,ty2)
+      | LocalRawDef(na1,def1), LocalRawDef(na2,def2) ->
+          check_same_binder ([na1],def1) ([na2],def2)          
+      | _ -> failwith "not same binder") bl1 bl2
+
+let same c d = try check_same_type c d; true with _ -> false
+
+(* Idem for rawconstr *)
+let option_iter2 f o1 o2 = 
+  match o1, o2 with
+      Some o1, Some o2 -> f o1 o2
+    | None, None -> ()
+    | _ -> failwith "option"
+
+let array_iter2 f v1 v2 =
+  List.iter2 f (Array.to_list v1) (Array.to_list v2)
+
+let rec same_patt p1 p2 =
+  match p1, p2 with
+      PatVar(_,na1), PatVar(_,na2) -> if na1<>na2 then failwith "PatVar"
+    | PatCstr(_,c1,pl1,al1), PatCstr(_,c2,pl2,al2) ->
+        if c1<>c2 || al1 <> al2 then failwith "PatCstr";
+        List.iter2 same_patt pl1 pl2
+    | _ -> failwith "same_patt"
+
+let rec same_raw c d =
+  match c,d with
+   | RRef(_,gr1), RRef(_,gr2) -> if gr1<>gr2 then failwith "RRef"
+   | RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar"
+   | REvar(_,e1,a1), REvar(_,e2,a2) ->
+       if e1 <> e2 then failwith "REvar";
+       option_iter2(List.iter2 same_raw) a1 a2
+  | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar"
+  | RApp(_,f1,a1), RApp(_,f2,a2) ->
+      List.iter2 same_raw (f1::a1) (f2::a2)
+  | RLambda(_,na1,t1,m1), RLambda(_,na2,t2,m2) ->
+      if na1 <> na2 then failwith "RLambda";
+      same_raw t1 t2; same_raw m1 m2
+  | RProd(_,na1,t1,m1), RProd(_,na2,t2,m2) ->
+      if na1 <> na2 then failwith "RProd";
+      same_raw t1 t2; same_raw m1 m2
+  | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) ->
+      if na1 <> na2 then failwith "RLetIn";
+      same_raw t1 t2; same_raw m1 m2
+  | RCases(_,_,c1,b1), RCases(_,_,c2,b2) ->
+      List.iter2
+        (fun (t1,{contents=(al1,oind1)}) (t2,{contents=(al2,oind2)}) ->
+          same_raw t1 t2;
+          if al1 <> al2 then failwith "RCases";
+          option_iter2(fun (_,i1,nl1) (_,i2,nl2) ->
+            if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2;
+      List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) ->
+        List.iter2 same_patt pl1 pl2;
+        same_raw b1 b2) b1 b2
+  | ROrderedCase(_,_,_,c1,v1,_), ROrderedCase(_,_,_,c2,v2,_) ->
+      same_raw c1 c2;
+      array_iter2 same_raw v1 v2
+  | RLetTuple(_,nl1,_,b1,c1), RLetTuple(_,nl2,_,b2,c2) ->
+      if nl1<>nl2 then failwith "RLetTuple";
+      same_raw b1 b2;
+      same_raw c1 c2
+  | RIf(_,b1,_,t1,e1),RIf(_,b2,_,t2,e2) ->
+      same_raw b1 b2; same_raw t1 t2; same_raw e1 e2
+  | RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) ->
+      if fk1 <> fk2 || na1 <> na2 then failwith "RRec";
+      array_iter2
+        (List.iter2 (fun (na1,bd1,ty1) (na2,bd2,ty2) ->
+          if na1<>na2 then failwith "RRec";
+          option_iter2 same_raw bd1 bd2;
+          same_raw ty1 ty2)) bl1 bl2;
+      array_iter2 same_raw ty1 ty2;
+      array_iter2 same_raw def1 def2
+  | RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort"
+  | RHole _, _ -> ()
+  | _, RHole _ -> ()
+  | RCast(_,c1,_),r2 -> same_raw c1 r2
+  | r1, RCast(_,c2,_) -> same_raw r1 c2
+  | RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic"
+  | _ -> failwith "same_raw"
+     
+let same_rawconstr c d = 
+  try same_raw c d; true
+  with Failure _ | Invalid_argument _ -> false
+
+(**********************************************************************)
+(* mapping patterns to cases_pattern_expr                                *)
+
+let make_current_scopes (scopt,scopes) = 
+  option_fold_right push_scope scopt scopes
+
+let has_curly_brackets ntn =
+  String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or
+    String.sub ntn (String.length ntn - 6) 6 = " { _ }" or
+    string_string_contains ntn " { _ } ")
+
+let rec wildcards ntn n =
+  if n = String.length ntn then []
+  else let l = spaces ntn (n+1) in if ntn.[n] = '_' then n::l else l
+and spaces ntn n =
+  if n = String.length ntn then []
+  else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
+
+let expand_curly_brackets make_ntn ntn l =
+  let ntn' = ref ntn in
+  let rec expand_ntn i =
+    function
+    | [] -> []
+    | a::l ->
+        let a' = 
+          let p = List.nth (wildcards !ntn' 0) i - 2 in
+          if p>=0 & p+5 <= String.length !ntn' & String.sub !ntn' p 5 = "{ _ }"
+          then begin
+            ntn' := 
+              String.sub !ntn' 0 p ^ "_" ^ 
+              String.sub !ntn' (p+5) (String.length !ntn' -p-5);
+            make_ntn "{ _ }" [a] end
+          else a in
+        a' :: expand_ntn (i+1) l in
+  let l = expand_ntn 0 l in
+  (* side effect *)
+  make_ntn !ntn' l
+
+let make_notation loc ntn l =
+  if has_curly_brackets ntn
+  then expand_curly_brackets (fun n l -> CNotation (loc,n,l)) ntn l
+  else match ntn,l with
+    (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
+    | "- _", [CNumeral(_,Bignat.POS p)] ->
+        CNotation (loc,ntn,[CNotation(loc,"( _ )",l)])
+    | _ -> CNotation (loc,ntn,l)
+
+let make_pat_notation loc ntn l =
+  if has_curly_brackets ntn
+  then expand_curly_brackets (fun n l -> CPatNotation (loc,n,l)) ntn l
+  else match ntn,l with
+    (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
+    | "- _", [CPatNumeral(_,Bignat.POS p)] ->
+        CPatNotation (loc,ntn,[CPatNotation(loc,"( _ )",l)])
+    | _ -> CPatNotation (loc,ntn,l)
+
+
+(*
+let rec cases_pattern_expr_of_constr_expr = function
+  | CRef r -> CPatAtom (dummy_loc,Some r)
+  | CHole loc -> CPatAtom (loc,None)
+  | CApp (loc,(proj,CRef c),l) when proj = None ->
+      let l,e = List.split l in
+      if not (List.for_all ((=) None) e) then
+	anomaly "Unexpected explicitation in pattern";
+      CPatCstr (loc,c,List.map cases_pattern_expr_of_constr_expr l)
+  | CNotation (loc,ntn,l) ->
+      CPatNotation (loc,ntn,List.map cases_pattern_expr_of_constr_expr l)
+  | CNumeral (loc,n) -> CPatNumeral (loc,n)
+  | CDelimiters (loc,s,e) -> 
+      CPatDelimiters (loc,s,cases_pattern_expr_of_constr_expr e)	
+  | _ -> anomaly "Constrextern: not a pattern"
+
+let rec rawconstr_of_cases_pattern = function
+  | PatVar (loc,Name id) -> RVar (loc,id)
+  | PatVar (loc,Anonymous) -> RHole (loc,InternalHole)
+  | PatCstr (loc,(ind,_ as c),args,_) -> 
+      let nparams = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in
+      let params = list_tabulate (fun _ -> RHole (loc,InternalHole)) nparams in
+      let args = params @ List.map rawconstr_of_cases_pattern args in
+      let f = RRef (loc,ConstructRef c) in
+      if args = [] then f else RApp (loc,f,args)
+*)
+
+let bind_env sigma var v =
+  try
+    let vvar = List.assoc var sigma in
+    if v=vvar then sigma else raise No_match
+  with Not_found ->
+    (* TODO: handle the case of multiple occs in different scopes *)
+    (var,v)::sigma
+
+let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
+  | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
+  | PatVar (_,Anonymous), AHole _ -> sigma
+  | a, AHole _ when not(Options.do_translate()) -> sigma
+  | PatCstr (loc,(ind,_ as r1),args1,Anonymous), _ ->
+      let nparams =
+	(snd (Global.lookup_inductive ind)).Declarations.mind_nparams in
+      let l2 =
+        match a2 with
+	  | ARef (ConstructRef r2) when r1 = r2 -> []
+	  | AApp (ARef (ConstructRef r2),l2)  when r1 = r2 -> l2
+          | _ -> raise No_match in
+      if List.length l2 <> nparams + List.length args1
+      then raise No_match
+      else
+        let (p2,args2) = list_chop nparams l2 in
+        (* All parameters must be _ *)
+        List.iter (function AHole _ -> () | _ -> raise No_match) p2;
+	List.fold_left2 (match_cases_pattern metas) sigma args1 args2
+  | _ -> raise No_match
+
+let match_aconstr_cases_pattern c (metas_scl,pat) =
+  let subst = match_cases_pattern (List.map fst metas_scl) [] c pat in
+  (* Reorder canonically the substitution *)
+  let find x subst =
+    try List.assoc x subst
+    with Not_found -> anomaly "match_aconstr_cases_pattern" in
+  List.map (fun (x,scl) -> (find x subst,scl)) metas_scl
+
+ (* Better to use extern_rawconstr composed with injection/retraction ?? *)
+let rec extern_cases_pattern_in_scope scopes vars pat =
+  try 
+    if !Options.raw_print or !print_no_symbol then raise No_match;
+    let (sc,n) = Symbols.uninterp_cases_numeral pat in
+    match Symbols.availability_of_numeral sc (make_current_scopes scopes) with
+    | None -> raise No_match
+    | Some key ->
+        let loc = pattern_loc pat in
+        insert_pat_delimiters (CPatNumeral (loc,n)) key
+  with No_match ->
+  try 
+    if !Options.raw_print or !print_no_symbol then raise No_match;
+    extern_symbol_pattern scopes vars pat
+      (Symbols.uninterp_cases_pattern_notations pat)
+  with No_match ->
+  match pat with
+  | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,v7_to_v8_id id)))
+  | PatVar (loc,Anonymous) -> CPatAtom (loc, None) 
+  | PatCstr(loc,cstrsp,args,na) ->
+      let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
+      let p = CPatCstr
+        (loc,extern_reference loc vars (ConstructRef cstrsp),args) in
+      (match na with
+	| Name id -> CPatAlias (loc,p,v7_to_v8_id id)
+	| Anonymous -> p)
+	
+and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
+  | [] -> raise No_match
+  | (keyrule,pat,n as rule)::rules ->
+      try
+	(* Check the number of arguments expected by the notation *)
+	let loc = match t,n with
+	  | PatCstr (_,f,l,_), Some n when List.length l > n ->
+	      raise No_match
+	  | PatCstr (loc,_,_,_),_ -> loc
+	  | PatVar (loc,_),_ -> loc in
+	(* Try matching ... *)
+	let subst = match_aconstr_cases_pattern t pat in
+	(* Try availability of interpretation ... *)
+        match keyrule with
+          | NotationRule (sc,ntn) ->
+	      let scopes' = make_current_scopes (tmp_scope, scopes) in
+	      (match Symbols.availability_of_notation (sc,ntn) scopes' with
+                  (* Uninterpretation is not allowed in current context *)
+              | None -> raise No_match
+                  (* Uninterpretation is allowed in current context *)
+	      | Some (scopt,key) ->
+	          let scopes = make_current_scopes (scopt, scopes) in
+	          let l =
+		    List.map (fun (c,(scopt,scl)) ->
+		      extern_cases_pattern_in_scope 
+		        (scopt,List.fold_right push_scope scl scopes) vars c)
+                      subst in
+		  insert_pat_delimiters (make_pat_notation loc ntn l) key)
+          | SynDefRule kn ->
+ 	      CPatAtom (loc,Some (Qualid (loc, shortest_qualid_of_syndef kn)))
+      with
+	  No_match -> extern_symbol_pattern allscopes vars t rules
+
+(**********************************************************************)
+(* Externalising applications *)
+
+let occur_name na aty =
+  match na with
+    | Name id -> occur_var_constr_expr id aty
+    | Anonymous -> false
+
+let is_projection nargs = function
+  | Some r when not !Options.raw_print & !print_projections ->
+      (try 
+	let n = Recordops.find_projection_nparams r + 1 in
+	if n <= nargs then Some n else None
+      with Not_found -> None)
+  | _ -> None
+
+let is_nil = function
+  | [CRef ref] -> snd (repr_qualid (snd (qualid_of_reference ref))) = id_of_string "nil"
+  | _ -> false
+
+let stdlib_but_length args = function
+  | Some r -> 
+      let dir,id = repr_path (sp_of_global r) in
+      (is_coq_root (Lib.library_dp()) or is_coq_root dir)
+      && not (List.mem (string_of_id id) ["Zlength";"length"] && is_nil args)
+      && not (List.mem (string_of_id id) ["In"] && List.length args >= 2
+              && is_nil (List.tl args))
+  | None -> false
+
+let explicit_code imp q =
+  dummy_loc,
+  if !Options.v7 & not (Options.do_translate()) then ExplByPos q
+  else ExplByName (name_of_implicit imp)
+
+let is_hole = function CHole _ -> true | _ -> false
+
+let is_significant_implicit a impl tail =
+  not (is_hole a) or (tail = [] & not (List.for_all is_status_implicit impl))
+
+(* Implicit args indexes are in ascending order *)
+(* inctx is useful only if there is a last argument to be deduced from ctxt *)
+let explicitize loc inctx impl (cf,f) args =
+  let n = List.length args in
+  let rec exprec q = function
+    | a::args, imp::impl when is_status_implicit imp ->
+        let tail = exprec (q+1) (args,impl) in
+        let visible =
+          !Options.raw_print or
+          (!print_implicits & !print_implicits_explicit_args) or 
+	  (is_significant_implicit a impl tail &
+	  (not (is_inferable_implicit inctx n imp) or
+	    (Options.do_translate() & not (stdlib_but_length args cf))))
+	in
+        if visible then (a,Some (explicit_code imp q)) :: tail else tail
+    | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl)
+    | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*)
+    | [], _ -> [] in
+  match is_projection (List.length args) cf with
+    | Some i as ip ->
+	if impl <> [] & is_status_implicit (List.nth impl (i-1)) then
+	  let f' = match f with CRef f -> f | _ -> assert false in
+	  CAppExpl (loc,(ip,f'),args)
+	else
+	  let (args1,args2) = list_chop i args in
+	  let (impl1,impl2) = if impl=[] then [],[] else list_chop i impl in
+	  let args1 = exprec 1 (args1,impl1) in
+	  let args2 = exprec (i+1) (args2,impl2) in
+	  CApp (loc,(Some (List.length args1),f),args1@args2)
+    | None -> 
+	let args = exprec 1 (args,impl) in
+	if args = [] then f else CApp (loc, (None, f), args)
+
+let extern_global loc impl f =
+  if impl <> [] & List.for_all is_status_implicit impl then
+    CAppExpl (loc, (None, f), [])
+  else
+    CRef f
+
+let extern_app loc inctx impl (cf,f) args =
+  if args = [] (* maybe caused by a hidden coercion *) then
+    extern_global loc impl f
+  else
+  if 
+    ((!Options.raw_print or
+      (!print_implicits & not !print_implicits_explicit_args)) &
+     List.exists is_status_implicit impl)
+  then 
+    CAppExpl (loc, (is_projection (List.length args) cf, f), args)
+  else
+    explicitize loc inctx impl (cf,CRef f) args
+
+let rec extern_args extern scopes env args subscopes =
+  match args with
+    | [] -> []
+    | a::args ->
+	let argscopes, subscopes = match subscopes with
+	  | [] -> (None,scopes), []
+	  | scopt::subscopes -> (scopt,scopes), subscopes in
+	extern argscopes env a :: extern_args extern scopes env args subscopes
+
+let rec remove_coercions inctx = function
+  | RApp (loc,RRef (_,r),args) as c
+      when
+        inctx &
+        not (!Options.raw_print or !print_coercions or Options.do_translate ())
+      ->
+      (try match Classops.hide_coercion r with
+	  | Some n when n < List.length args ->
+	      (* We skip a coercion *) 
+	      let l = list_skipn n args in
+              let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
+              let (a,l) =
+                (* Recursively remove the head coercions *)
+                match remove_coercions inctx a with
+                  | RApp (_,a,l') -> a,l'@l
+                  | a -> a,l in
+              if l = [] then a
+              else
+                (* Recursively remove coercions in arguments *)
+                RApp (loc,a,List.map (remove_coercions true) l)
+	  | _ -> c
+      with Not_found -> c)
+  | c -> c
+
+let rec rename_rawconstr_var id0 id1 = function
+    RRef(loc,VarRef id) when id=id0 -> RRef(loc,VarRef id1)
+  | RVar(loc,id) when id=id0 -> RVar(loc,id1)
+  | c -> map_rawconstr (rename_rawconstr_var id0 id1) c
+
+let rec share_fix_binders n rbl ty def =
+  match ty,def with
+      RProd(_,na0,t0,b), RLambda(_,na1,t1,m) ->
+        if not(same_rawconstr t0 t1) then List.rev rbl, ty, def
+        else
+          let (na,b,m) =
+            match na0, na1 with
+                Name id0, Name id1 ->
+                  if id0=id1 then (na0,b,m)
+                  else if not (occur_rawconstr id1 b) then
+                    (na1,rename_rawconstr_var id0 id1 b,m)
+                  else if not (occur_rawconstr id0 m) then
+                    (na1,b,rename_rawconstr_var id1 id0 m)
+                  else (* vraiment pas de chance! *)
+                    failwith "share_fix_binders: capture"
+              | Name id, Anonymous ->
+                  if not (occur_rawconstr id m) then (na0,b,m)
+                  else
+                    failwith "share_fix_binders: capture"
+              | Anonymous, Name id -> 
+                  if not (occur_rawconstr id b) then (na1,b,m)
+                  else
+                    failwith "share_fix_binders: capture"
+              | _ -> (na1,b,m) in
+          share_fix_binders (n-1) ((na,None,t0)::rbl) b m
+    | _ -> List.rev rbl, ty, def
+
+(**********************************************************************)
+(* mapping rawterms to constr_expr                                    *)
+
+let rec extern inctx scopes vars r =
+  try 
+    if !Options.raw_print or !print_no_symbol then raise No_match;
+    extern_numeral (Rawterm.loc_of_rawconstr r)
+      scopes (Symbols.uninterp_numeral r)
+  with No_match ->
+
+  let r = remove_coercions inctx r in
+
+  try 
+    if !Options.raw_print or !print_no_symbol then raise No_match;
+    extern_symbol scopes vars r (Symbols.uninterp_notations r)
+  with No_match -> match r with
+  | RRef (loc,ref) ->
+      extern_global loc (implicits_of_global_out ref)
+        (extern_reference loc vars ref)
+
+  | RVar (loc,id) -> CRef (Ident (loc,v7_to_v8_id id))
+
+  | REvar (loc,n,_) -> (* we drop args *) extern_evar loc n
+
+  | RPatVar (loc,n) -> if !print_meta_as_hole then CHole loc else CPatVar (loc,n)
+
+  | RApp (loc,f,args) ->
+      (match f with
+	 | RRef (rloc,ref) ->
+	     let subscopes = Symbols.find_arguments_scope ref in
+	     let args =
+	       extern_args (extern true) (snd scopes) vars args subscopes in
+	     extern_app loc inctx (implicits_of_global_out ref)
+               (Some ref,extern_reference rloc vars ref)
+	       args
+	 | RVar (rloc,id) -> (* useful for translation of inductive *)
+	     let args = List.map (sub_extern true scopes vars) args in
+	     extern_app loc inctx (get_temporary_implicits_out id)
+	       (None,Ident (rloc,v7_to_v8_id id))
+	       args
+	 | _       -> 
+	     explicitize loc inctx [] (None,sub_extern false scopes vars f)
+               (List.map (sub_extern true scopes vars) args))
+
+  | RProd (loc,Anonymous,t,c) ->
+      (* Anonymous product are never factorized *)
+      CArrow (loc,extern_type scopes vars t, extern_type scopes vars c)
+
+  | RLetIn (loc,na,t,c) ->
+      let na = name_app translate_ident na in
+      CLetIn (loc,(loc,na),sub_extern false scopes vars t,
+              extern inctx scopes (add_vname vars na) c)
+
+  | RProd (loc,na,t,c) ->
+      let t = extern_type scopes vars (anonymize_if_reserved na t) in
+      let (idl,c) = factorize_prod scopes (add_vname vars na) t c in
+      CProdN (loc,[(dummy_loc,na)::idl,t],c)
+
+  | RLambda (loc,na,t,c) ->
+      let t = extern_type scopes vars (anonymize_if_reserved na t) in
+      let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
+      CLambdaN (loc,[(dummy_loc,na)::idl,t],c)
+
+  | RCases (loc,(typopt,rtntypopt),tml,eqns) ->
+      let pred = option_app (extern_type scopes vars) typopt in
+      let vars' = 
+	List.fold_right (name_fold Idset.add)
+	  (cases_predicate_names tml) vars in
+      let rtntypopt' = option_app (extern_type scopes vars') !rtntypopt in
+      let tml = List.map (fun (tm,{contents=(na,x)}) ->
+        let na' = match na,tm with
+            Anonymous, RVar (_,id) when 
+              !rtntypopt<>None & occur_rawconstr id (out_some !rtntypopt)
+              -> Some Anonymous
+          | Anonymous, _ -> None
+          | Name id, RVar (_,id') when id=id' -> None
+          | Name _, _ -> Some na in
+	(sub_extern false scopes vars tm,
+	(na',option_app (fun (loc,ind,nal) ->
+	  let args = List.map (function
+	    | Anonymous -> RHole (dummy_loc,InternalHole) 
+	    | Name id -> RVar (dummy_loc,id)) nal in
+	  let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),args) in
+	  (extern_type scopes vars t)) x))) tml in
+      let eqns = List.map (extern_eqn (typopt<>None) scopes vars) eqns in 
+      CCases (loc,(pred,rtntypopt'),tml,eqns)
+
+  | ROrderedCase (loc,cs,typopt,tm,bv,{contents = Some x}) ->
+      extern false scopes vars x
+
+  | ROrderedCase (loc,IfStyle,typopt,tm,bv,_) when Options.do_translate () ->
+      let rec strip_branches = function
+        | (RLambda (_,_,_,c1), RLambda (_,_,_,c2)) -> strip_branches (c1,c2)
+        | x -> x in
+      let c1,c2 = strip_branches (bv.(0),bv.(1)) in
+      msgerrnl (str "Warning: unable to ensure the correctness of the translation of an if-then-else");
+      let bv = Array.map (sub_extern (typopt<>None) scopes vars) [|c1;c2|] in
+      COrderedCase
+	(loc,IfStyle,option_app (extern_type scopes vars) typopt,
+         sub_extern false scopes vars tm,Array.to_list bv)
+      (* We failed type-checking If and to translate it to CIf *)
+      (* try to remove the dependances in branches anyway *)
+
+
+  | ROrderedCase (loc,cs,typopt,tm,bv,_) ->
+      let bv = Array.map (sub_extern (typopt<>None) scopes vars) bv in
+      COrderedCase
+	(loc,cs,option_app (extern_type scopes vars) typopt,
+         sub_extern false scopes vars tm,Array.to_list bv)
+
+  | RLetTuple (loc,nal,(na,typopt),tm,b) ->
+      CLetTuple (loc,nal,
+        (Some na,option_app (extern_type scopes (add_vname vars na)) typopt),
+        sub_extern false scopes vars tm,
+        extern false scopes (List.fold_left add_vname vars nal) b)
+
+  | RIf (loc,c,(na,typopt),b1,b2) ->
+      CIf (loc,sub_extern false scopes vars c,
+        (Some na,option_app (extern_type scopes (add_vname vars na)) typopt),
+        sub_extern false scopes vars b1, sub_extern false scopes vars b2)
+
+  | RRec (loc,fk,idv,blv,tyv,bv) ->
+      let vars' = Array.fold_right Idset.add idv vars in
+      (match fk with
+	 | RFix (nv,n) ->
+	     let listdecl = 
+	       Array.mapi (fun i fi ->
+                 let (bl,ty,def) =
+                   if Options.do_translate() then
+                     let n = List.fold_left
+                       (fun n (_,obd,_) -> if obd=None then n-1 else n)
+                       nv.(i) blv.(i) in
+                     share_fix_binders n (List.rev blv.(i)) tyv.(i) bv.(i)
+                   else blv.(i), tyv.(i), bv.(i) in
+                 let (ids,bl) = extern_local_binder scopes vars bl in
+                 let vars0 = List.fold_right (name_fold Idset.add) ids vars in
+                 let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
+		 (fi,nv.(i), bl, extern_type scopes vars0 ty,
+                  extern false scopes vars1 def)) idv
+	     in 
+	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
+	 | RCoFix n -> 
+	     let listdecl =
+               Array.mapi (fun i fi ->
+                 let (ids,bl) = extern_local_binder scopes vars blv.(i) in
+                 let vars0 = List.fold_right (name_fold Idset.add) ids vars in
+                 let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
+		 (fi,bl,extern_type scopes vars0 tyv.(i),
+                  sub_extern false scopes vars1 bv.(i))) idv
+	     in
+	     CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
+
+  | RSort (loc,s) ->
+      let s = match s with
+	 | RProp _ -> s
+	 | RType (Some _) when !print_universes -> s
+	 | RType _ -> RType None in
+      CSort (loc,s)
+
+  | RHole (loc,e) -> CHole loc
+
+  | RCast (loc,c,t) ->
+      CCast (loc,sub_extern true scopes vars c,extern_type scopes vars t)
+
+  | RDynamic (loc,d) -> CDynamic (loc,d)
+
+and extern_type (_,scopes) = extern true (Some Symbols.type_scope,scopes)
+
+and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
+
+and factorize_prod scopes vars aty = function
+  | RProd (loc,(Name id as na),ty,c)
+      when same aty (extern_type scopes vars (anonymize_if_reserved na ty))
+	& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
+	-> let id = translate_ident id in
+           let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in
+           ((loc,Name id)::nal,c)
+  | c -> ([],extern_type scopes vars c)
+
+and factorize_lambda inctx scopes vars aty = function
+  | RLambda (loc,na,ty,c)
+      when same aty (extern_type scopes vars (anonymize_if_reserved na ty))
+	& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
+	-> let na = name_app translate_ident na in
+           let (nal,c) =
+	     factorize_lambda inctx scopes (add_vname vars na) aty c in
+           ((loc,na)::nal,c)
+  | c -> ([],sub_extern inctx scopes vars c)
+
+and extern_local_binder scopes vars = function
+    [] -> ([],[])
+  | (na,Some bd,ty)::l ->
+      let na = name_app translate_ident na in
+      let (ids,l) =
+        extern_local_binder scopes (name_fold Idset.add na vars) l in
+      (na::ids,
+       LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l)
+      
+  | (na,None,ty)::l ->
+      let na = name_app translate_ident na in
+      let ty = extern_type scopes vars (anonymize_if_reserved na ty) in
+      (match extern_local_binder scopes (name_fold Idset.add na vars) l with
+          (ids,LocalRawAssum(nal,ty')::l)
+            when same ty ty' &
+              match na with Name id -> not (occur_var_constr_expr id ty')
+                | _ -> true ->
+              (na::ids,
+               LocalRawAssum((dummy_loc,na)::nal,ty')::l)
+        | (ids,l) ->
+            (na::ids,
+             LocalRawAssum([(dummy_loc,na)],ty) :: l))
+
+and extern_eqn inctx scopes vars (loc,ids,pl,c) =
+  (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl,
+   extern inctx scopes vars c)
+
+and extern_numeral loc scopes (sc,n) =
+  match Symbols.availability_of_numeral sc (make_current_scopes scopes) with
+    | None -> raise No_match
+    | Some key -> insert_delimiters (CNumeral (loc,n)) key
+
+and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
+  | [] -> raise No_match
+  | (keyrule,pat,n as rule)::rules ->
+      let loc = Rawterm.loc_of_rawconstr t in
+      try
+	(* Adjusts to the number of arguments expected by the notation *)
+	let (t,args) = match t,n with
+	  | RApp (_,f,args), Some n when List.length args > n ->
+	      let args1, args2 = list_chop n args in
+	      RApp (dummy_loc,f,args1), args2
+	  | _ -> t,[] in
+	(* Try matching ... *)
+	let subst = match_aconstr t pat in
+	(* Try availability of interpretation ... *)
+        let e =
+          match keyrule with
+          | NotationRule (sc,ntn) ->
+	      let scopes' = make_current_scopes (tmp_scope, scopes) in
+	      (match Symbols.availability_of_notation (sc,ntn) scopes' with
+                  (* Uninterpretation is not allowed in current context *)
+              | None -> raise No_match
+                  (* Uninterpretation is allowed in current context *)
+	      | Some (scopt,key) ->
+	          let scopes = make_current_scopes (scopt, scopes) in
+	          let l =
+		    List.map (fun (c,(scopt,scl)) ->
+		      extern (* assuming no overloading: *) true
+		        (scopt,List.fold_right push_scope scl scopes) vars c)
+                      subst in
+	          insert_delimiters (make_notation loc ntn l) key)
+          | SynDefRule kn ->
+              CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in
+ 	if args = [] then e 
+	else
+	  (* TODO: compute scopt for the extra args, in case, head is a ref *)
+	  explicitize loc false [] (None,e)
+	  (List.map (extern true allscopes vars) args)
+      with
+	  No_match -> extern_symbol allscopes vars t rules
+
+let extern_rawconstr vars c = 
+  extern false (None,Symbols.current_scopes()) vars c
+
+let extern_rawtype vars c =
+  extern_type (None,Symbols.current_scopes()) vars c
+
+let extern_cases_pattern vars p = 
+  extern_cases_pattern_in_scope (None,Symbols.current_scopes()) vars p
+
+(******************************************************************)
+(* Main translation function from constr -> constr_expr *)
+
+let loc = dummy_loc (* for constr and pattern, locations are lost *)
+
+let extern_constr_gen at_top scopt env t =
+  let vars = vars_of_env env in
+  let avoid = if at_top then ids_of_context env else [] in
+  extern (not at_top) (scopt,Symbols.current_scopes()) vars
+    (Detyping.detype (at_top,env) avoid (names_of_rel_context env) t)
+
+let extern_constr_in_scope at_top scope env t =
+  extern_constr_gen at_top (Some scope) env t
+
+let extern_constr at_top env t =
+  extern_constr_gen at_top None env t
+
+(******************************************************************)
+(* Main translation function from pattern -> constr_expr *)
+
+let rec raw_of_pat tenv env = function
+  | PRef ref -> RRef (loc,ref)
+  | PVar id -> RVar (loc,id)
+  | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat tenv env) l))
+  | PRel n ->
+      let id = try match lookup_name_of_rel n env with
+	| Name id   -> id
+	| Anonymous ->
+	    anomaly "rawconstr_of_pattern: index to an anonymous variable"
+      with Not_found -> id_of_string ("[REL "^(string_of_int n)^"]") in
+      RVar (loc,id)
+  | PMeta None -> RHole (loc,InternalHole)
+  | PMeta (Some n) -> RPatVar (loc,(false,n))
+  | PApp (f,args) ->
+      RApp (loc,raw_of_pat tenv env f,array_map_to_list (raw_of_pat tenv env) args)
+  | PSoApp (n,args) ->
+      RApp (loc,RPatVar (loc,(true,n)),
+        List.map (raw_of_pat tenv env) args)
+  | PProd (na,t,c) ->
+      RProd (loc,na,raw_of_pat tenv env t,raw_of_pat tenv (na::env) c)
+  | PLetIn (na,t,c) ->
+      RLetIn (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c)
+  | PLambda (na,t,c) ->
+      RLambda (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c)
+  | PCase ((_,(IfStyle|LetStyle as cs)),typopt,tm,bv) ->
+      ROrderedCase (loc,cs,option_app (raw_of_pat tenv env) typopt,
+         raw_of_pat tenv env tm,Array.map (raw_of_pat tenv env) bv, ref None)
+  | PCase ((_,cs),typopt,tm,[||]) ->
+      RCases (loc,(option_app (raw_of_pat tenv env) typopt,ref None (* TODO *)),
+         [raw_of_pat tenv env tm,ref (Anonymous,None)],[])
+  | PCase ((Some ind,cs),typopt,tm,bv) ->
+      let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
+      let k = (snd (lookup_mind_specif (Global.env()) ind)).Declarations.mind_nrealargs in
+      Detyping.detype_case false (raw_of_pat tenv env)(raw_of_eqn tenv env)
+	(fun _ _ -> false (* lazy: don't try to display pattern with "if" *))
+	tenv avoid ind cs typopt k tm bv
+  | PCase _ -> error "Unsupported case-analysis while printing pattern"
+  | PFix f -> Detyping.detype (false,tenv) [] env (mkFix f)
+  | PCoFix c -> Detyping.detype (false,tenv) [] env (mkCoFix c)
+  | PSort s -> RSort (loc,s)
+
+and raw_of_eqn tenv env constr construct_nargs branch =
+  let make_pat x env b ids =
+    let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
+    let id = next_name_away_with_default "x" x avoid in
+    PatVar (dummy_loc,Name id),(Name id)::env,id::ids
+  in
+  let rec buildrec ids patlist env n b =
+    if n=0 then
+      (dummy_loc, ids, 
+       [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
+       raw_of_pat tenv env b)
+    else
+      match b with
+	| PLambda (x,_,b) -> 
+	    let pat,new_env,new_ids = make_pat x env b ids in
+            buildrec new_ids (pat::patlist) new_env (n-1) b
+
+	| PLetIn (x,_,b) -> 
+	    let pat,new_env,new_ids = make_pat x env b ids in
+            buildrec new_ids (pat::patlist) new_env (n-1) b
+
+	| _ ->
+	    error "Unsupported branch in case-analysis while printing pattern"
+  in 
+  buildrec [] [] env construct_nargs branch
+
+let extern_pattern tenv env pat =
+  extern true (None,Symbols.current_scopes()) Idset.empty
+    (raw_of_pat tenv env pat)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
new file mode 100644
index 00000000..ad1c4391
--- /dev/null
+++ b/interp/constrextern.mli
@@ -0,0 +1,77 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: constrextern.mli,v 1.11.2.2 2004/07/16 20:51:12 herbelin Exp $ *)
+
+(*i*)
+open Util
+open Names
+open Term
+open Termops
+open Sign
+open Environ
+open Libnames
+open Nametab
+open Rawterm
+open Pattern
+open Topconstr
+open Symbols
+(*i*)
+
+(* v7->v8 translation *)
+val id_of_v7_string : string -> identifier
+val v7_to_v8_id : identifier -> identifier (* v7->v8 translation *)
+val shortest_qualid_of_v7_global : Idset.t -> global_reference -> qualid
+val check_same_type : constr_expr -> constr_expr -> unit
+
+(* Translation of pattern, cases pattern, rawterm and term into syntax
+   trees for printing *)
+
+val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr
+val extern_rawconstr : Idset.t -> rawconstr -> constr_expr
+val extern_rawtype : Idset.t -> rawconstr -> constr_expr
+val extern_pattern : env -> names_context -> constr_pattern -> constr_expr
+
+(* If [b=true] in [extern_constr b env c] then the variables in the first 
+   level of quantification clashing with the variables in [env] are renamed *)
+
+val extern_constr : bool -> env -> constr -> constr_expr
+val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
+val extern_reference : loc -> Idset.t -> global_reference -> reference
+
+(* Printing options *)
+val print_implicits : bool ref
+val print_arguments : bool ref
+val print_evar_arguments : bool ref
+val print_coercions : bool ref
+val print_universes : bool ref
+val print_no_symbol : bool ref
+val print_projections : bool ref
+
+(* This governs printing of implicit arguments. If [with_implicits] is
+   on and not [with_arguments] then implicit args are printed prefixed
+   by "!"; if [with_implicits] and [with_arguments] are both on the
+   function and not the arguments is prefixed by "!" *)
+val with_implicits : ('a -> 'b) -> 'a -> 'b
+val with_arguments : ('a -> 'b) -> 'a -> 'b
+
+(* This forces printing of coercions *)
+val with_coercions : ('a -> 'b) -> 'a -> 'b
+
+(* This forces printing universe names of Type{.} *)
+val with_universes : ('a -> 'b) -> 'a -> 'b
+
+(* This suppresses printing of numeral and symbols *)
+val without_symbols : ('a -> 'b) -> 'a -> 'b
+
+(* This prints metas as anonymous holes *)
+val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b
+
+(* For v8 translation *)
+val set_temporary_implicits_out :
+  (identifier * Impargs.implicits_list) list -> unit
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
new file mode 100644
index 00000000..e1b916e1
--- /dev/null
+++ b/interp/constrintern.ml
@@ -0,0 +1,1165 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: constrintern.ml,v 1.58.2.2 2004/07/16 20:51:12 herbelin Exp $ *)
+
+open Pp
+open Util
+open Options
+open Names
+open Nameops
+open Libnames
+open Impargs
+open Rawterm
+open Pattern
+open Pretyping
+open Topconstr
+open Nametab
+open Symbols
+
+(* To interpret implicits and arg scopes of recursive variables in
+   inductive types and recursive definitions *)
+type var_internalisation_data =
+    identifier list * Impargs.implicits_list * scope_name option list
+
+type implicits_env = (identifier * var_internalisation_data) list
+type full_implicits_env = identifier list * implicits_env
+
+let interning_grammar = ref false
+
+(* Historically for parsing grammar rules, but in fact used only for
+   translator, v7 parsing, and unstrict tactic internalisation *)
+let for_grammar f x =
+  interning_grammar := true;
+  let a = f x in
+  interning_grammar := false;
+  a
+
+let variables_bind = ref false
+
+(* For the translator *)
+let temporary_implicits_in = ref []
+let set_temporary_implicits_in l = temporary_implicits_in := l
+
+(**********************************************************************)
+(* Internalisation errors                                             *)
+
+type internalisation_error =
+  | VariableCapture of identifier
+  | WrongExplicitImplicit
+  | NegativeMetavariable
+  | NotAConstructor of reference
+  | UnboundFixName of bool * identifier
+  | NonLinearPattern of identifier
+  | BadPatternsNumber of int * int
+  | BadExplicitationNumber of explicitation * int option
+
+exception InternalisationError of loc * internalisation_error
+
+let explain_variable_capture id =
+  str "The variable " ++ pr_id id ++ str " occurs in its type"
+
+let explain_wrong_explicit_implicit =
+  str "Found an explicitly given implicit argument but was expecting" ++
+  fnl () ++ str "a regular one"
+
+let explain_negative_metavariable =
+  str "Metavariable numbers must be positive"
+
+let explain_not_a_constructor ref =
+  str "Unknown constructor: " ++ pr_reference ref
+
+let explain_unbound_fix_name is_cofix id =
+  str "The name" ++ spc () ++ pr_id id ++ 
+  spc () ++ str "is not bound in the corresponding" ++ spc () ++
+  str (if is_cofix then "co" else "") ++ str "fixpoint definition"
+
+let explain_non_linear_pattern id =
+  str "The variable " ++ pr_id id ++ str " is bound several times in pattern"
+
+let explain_bad_patterns_number n1 n2 =
+  let s = if n1 > 1 then "s" else "" in
+  str "Expecting " ++ int n1 ++ str " pattern" ++ str s ++ str " but found "
+    ++ int n2
+
+let explain_bad_explicitation_number n po =
+  match n with
+  | ExplByPos n ->
+      let s = match po with
+	| None -> str "a regular argument"
+	| Some p -> int p in
+      str "Bad explicitation number: found " ++ int n ++ 
+      str" but was expecting " ++ s
+  | ExplByName id ->
+      let s = match po with
+	| None -> str "a regular argument"
+	| Some p -> (*pr_id (name_of_position p) in*) failwith "" in
+      str "Bad explicitation name: found " ++ pr_id id ++ 
+      str" but was expecting " ++ s
+
+let explain_internalisation_error = function
+  | VariableCapture id -> explain_variable_capture id
+  | WrongExplicitImplicit -> explain_wrong_explicit_implicit
+  | NegativeMetavariable -> explain_negative_metavariable
+  | NotAConstructor ref -> explain_not_a_constructor ref
+  | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
+  | NonLinearPattern id -> explain_non_linear_pattern id
+  | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
+  | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po
+
+let error_unbound_patvar loc n =
+  user_err_loc
+    (loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++ 
+      str " is unbound")
+
+let error_bad_inductive_type loc =
+  user_err_loc (loc,"",str 
+    "This should be an inductive type applied to names or \"_\"")
+
+(**********************************************************************)
+(* Dump of globalization (to be used by coqdoc)                       *)
+let token_number = ref 0
+let last_pos = ref 0
+
+type coqdoc_state = Lexer.location_table * int * int
+
+let coqdoc_freeze () =
+  let lt = Lexer.location_table() in
+  let state = (lt,!token_number,!last_pos) in
+  token_number := 0;
+  last_pos := 0;
+  state
+
+let coqdoc_unfreeze (lt,tn,lp) =
+  Lexer.restore_location_table lt;
+  token_number := tn;
+  last_pos := lp
+
+let add_glob loc ref = 
+(*i
+  let sp = Nametab.sp_of_global (Global.env ()) ref in
+  let dir,_ = repr_path sp in
+  let rec find_module d = 
+    try 
+      let qid = let dir,id = split_dirpath d in make_qualid dir id in
+      let _ = Nametab.locate_loaded_library qid in d
+    with Not_found -> find_module (dirpath_prefix d) 
+  in
+  let s = string_of_dirpath (find_module dir) in
+  i*)
+  let sp = Nametab.sp_of_global ref in
+  let id = let _,id = repr_path sp in string_of_id id in
+  let dp = string_of_dirpath (Lib.library_part ref) in
+  dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) dp id)
+
+let loc_of_notation f loc args ntn =
+  if args=[] or ntn.[0] <> '_' then fst (unloc loc)
+  else snd (unloc (f (List.hd args)))
+
+let ntn_loc = loc_of_notation constr_loc
+let patntn_loc = loc_of_notation cases_pattern_loc
+
+let dump_notation_location =
+  fun pos ntn ((path,df),sc) ->
+    let rec next growing =
+      let loc = Lexer.location_function !token_number in
+      let (bp,_) = unloc loc in
+      if growing then if bp >= pos then loc else (incr token_number;next true)
+      else if bp = pos then loc
+      else if bp > pos then (decr token_number;next false)
+      else (incr token_number;next true) in
+    let loc = next (pos >= !last_pos) in
+    last_pos := pos;
+    let path = string_of_dirpath path in
+    let sc = match sc with Some sc -> " "^sc | None -> "" in
+    dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc)
+
+(**********************************************************************)
+(* Contracting "{ _ }" in notations *)
+
+let rec wildcards ntn n =
+  if n = String.length ntn then []
+  else let l = spaces ntn (n+1) in if ntn.[n] = '_' then n::l else l
+and spaces ntn n =
+  if n = String.length ntn then []
+  else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
+
+let expand_notation_string ntn n =
+  let pos = List.nth (wildcards ntn 0) n in
+  let hd = if pos = 0 then "" else String.sub ntn 0 pos in
+  let tl = 
+    if pos = String.length ntn then "" 
+    else String.sub ntn (pos+1) (String.length ntn - pos -1) in
+  hd ^ "{ _ }" ^ tl
+
+(* This contracts the special case of "{ _ }" for sumbool, sumor notations *)
+(* Remark: expansion of squash at definition is done in metasyntax.ml *)
+let contract_notation ntn l =
+  let ntn' = ref ntn in
+  let rec contract_squash n = function
+    | [] -> []
+    | CNotation (_,"{ _ }",[a]) :: l -> 
+        ntn' := expand_notation_string !ntn' n;
+        contract_squash n (a::l)
+    | a :: l ->
+        a::contract_squash (n+1) l in
+  let l = contract_squash 0 l in
+  (* side effect; don't inline *)
+  !ntn',l
+
+let contract_pat_notation ntn l =
+  let ntn' = ref ntn in
+  let rec contract_squash n = function
+    | [] -> []
+    | CPatNotation (_,"{ _ }",[a]) :: l -> 
+        ntn' := expand_notation_string !ntn' n;
+        contract_squash n (a::l)
+    | a :: l ->
+        a::contract_squash (n+1) l in
+  let l = contract_squash 0 l in
+  (* side effect; don't inline *)
+  !ntn',l
+
+(**********************************************************************)
+(* Remembering the parsing scope of variables in notations            *)
+
+let make_current_scope (scopt,scopes) = option_cons scopt scopes
+
+let set_var_scope loc id (_,scopt,scopes) varscopes =
+  let idscopes = List.assoc id varscopes in
+  if !idscopes <> None & 
+    make_current_scope (out_some !idscopes)
+    <> make_current_scope (scopt,scopes) then
+      user_err_loc (loc,"set_var_scope",
+      pr_id id ++ str " already occurs in a different scope")
+  else
+    idscopes := Some (scopt,scopes)
+
+(**********************************************************************)
+(* Discriminating between bound variables and global references       *)
+
+(* [vars1] is a set of name to avoid (used for the tactic language);
+   [vars2] is the set of global variables, env is the set of variables
+   abstracted until this point *)
+
+let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,_,impls) loc id =
+  let (vars1,unbndltacvars) = ltacvars in
+  (* Is [id] an inductive type potentially with implicit *)
+  try
+    let l,impl,argsc = List.assoc id impls in
+    let l = List.map 
+      (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
+    RVar (loc,id), impl, argsc,
+    (if !Options.v7 & !interning_grammar then [] else l)
+  with Not_found ->
+  (* Is [id] bound in current env or is an ltac var bound to constr *)
+  if Idset.mem id env or List.mem id vars1
+  then
+      RVar (loc,id), [], [], []
+  (* Is [id] a notation variable *)
+  else if List.mem_assoc id vars3
+  then
+    (set_var_scope loc id genv vars3; RVar (loc,id), [], [], [])
+  else
+
+  (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
+  try
+    match List.assoc id unbndltacvars with
+      | None -> user_err_loc (loc,"intern_var",
+	  pr_id id ++ str " ist not bound to a term")
+      | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
+  with Not_found ->
+  (* Is [id] a goal or section variable *)
+  let _ = Sign.lookup_named id vars2 in
+  try
+    (* [id] a section variable *)
+    (* Redundant: could be done in intern_qualid *)
+    let ref = VarRef id in
+    RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref, []
+  with _ ->
+    (* [id] a goal variable *)
+    RVar (loc,id), [], [], []
+
+let find_appl_head_data (_,_,_,_,impls) = function
+  | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
+  | x -> x,[],[],[]
+
+(* Is it a global reference or a syntactic definition? *)
+let intern_qualid loc qid =
+  try match Nametab.extended_locate qid with
+  | TrueGlobal ref ->
+      if !dump then add_glob loc ref;
+      RRef (loc, ref)
+  | SyntacticDef sp ->
+      Syntax_def.search_syntactic_definition loc sp
+  with Not_found ->
+    error_global_not_found_loc loc qid
+
+let intern_inductive r =
+  let loc,qid = qualid_of_reference r in
+  try match Nametab.extended_locate qid with
+  | TrueGlobal (IndRef ind) -> ind, []
+  | TrueGlobal _ -> raise Not_found
+  | SyntacticDef sp ->
+      (match Syntax_def.search_syntactic_definition loc sp with
+	| RApp (_,RRef(_,IndRef ind),l)
+	    when List.for_all (function RHole _ -> true | _ -> false) l ->
+	    (ind, List.map (fun _ -> Anonymous) l)
+	| _ -> raise Not_found)
+  with Not_found ->
+    error_global_not_found_loc loc qid
+
+let intern_reference env lvar = function
+  | Qualid (loc, qid) ->
+      find_appl_head_data lvar (intern_qualid loc qid)
+  | Ident (loc, id) ->
+      (* For old ast syntax compatibility *)
+      if (string_of_id id).[0] = '$' then RVar (loc,id),[],[],[] else
+      (* End old ast syntax compatibility *)
+      (* Pour traduction des implicites d'inductifs et points-fixes *)
+      try RVar (loc,id), List.assoc id !temporary_implicits_in, [], []
+      with Not_found ->
+      (* Fin pour traduction *)
+      try intern_var env lvar loc id
+      with Not_found -> 
+      try find_appl_head_data lvar (intern_qualid loc (make_short_qualid id))
+      with e ->
+	(* Extra allowance for non globalizing functions *)
+	if !interning_grammar then RVar (loc,id), [], [], []
+	else raise e
+
+let interp_reference vars r =
+  let (r,_,_,_) = intern_reference (Idset.empty,None,[]) (vars,[],[],[],[]) r 
+  in r
+
+let apply_scope_env (ids,_,scopes as env) = function
+  | [] -> (ids,None,scopes), []
+  | sc::scl -> (ids,sc,scopes), scl
+
+let rec adjust_scopes env scopes = function
+  | [] -> []
+  | a::args ->
+      let (enva,scopes) = apply_scope_env env scopes in
+      enva :: adjust_scopes env scopes args
+
+let rec simple_adjust_scopes = function
+  | _,[] -> []
+  | [],_::args -> None :: simple_adjust_scopes ([],args)
+  | sc::scopes,_::args -> sc :: simple_adjust_scopes (scopes,args)
+
+(**********************************************************************)
+(* Cases                                                              *)
+
+(* Check linearity of pattern-matching *)
+let rec has_duplicate = function 
+  | [] -> None
+  | x::l -> if List.mem x l then (Some x) else has_duplicate l
+
+let loc_of_lhs lhs = 
+ join_loc (cases_pattern_loc (List.hd lhs)) (cases_pattern_loc (list_last lhs))
+
+let check_linearity lhs ids =
+  match has_duplicate ids with
+    | Some id ->
+	raise (InternalisationError (loc_of_lhs lhs,NonLinearPattern id))
+    | None ->
+	()
+
+(* Warns if some pattern variable starts with uppercase *)
+let check_uppercase loc ids =
+(* A quoi ça sert ? Pour l'extraction vers ML ? Maintenant elle est externe
+  let is_uppercase_var v =
+    match (string_of_id v).[0] with 'A'..'Z' -> true | _  -> false
+  in
+  let warning_uppercase loc uplid =
+    let vars = h 0 (prlist_with_sep pr_coma pr_id uplid) in
+    let (s1,s2) = if List.length uplid = 1 then (" ","s ") else ("s "," ") in
+    warn (str ("the variable"^s1) ++ vars ++
+	  str (" start"^s2^"with an upper case letter in pattern")) in
+  let uplid = List.filter is_uppercase_var ids in
+  if uplid <> [] then warning_uppercase loc uplid
+*)
+  ()
+
+(* Match the number of pattern against the number of matched args *)
+let check_number_of_pattern loc n l =
+  let p = List.length l in
+  if n<>p then raise (InternalisationError (loc,BadPatternsNumber (n,p)))
+
+(* Manage multiple aliases *)
+
+  (* [merge_aliases] returns the sets of all aliases encountered at this
+     point and a substitution mapping extra aliases to the first one *)
+let merge_aliases (ids,subst as aliases) id =
+  ids@[id], if ids=[] then subst else (id, List.hd ids)::subst
+
+let alias_of = function
+  | ([],_) -> Anonymous
+  | (id::_,_) -> Name id
+
+let message_redundant_alias (id1,id2) =
+  if_verbose warning 
+   ("Alias variable "^(string_of_id id1)^" is merged with "^(string_of_id id2))
+
+(* Expanding notations *)
+
+let decode_patlist_value = function
+  | CPatCstr (_,_,l) -> l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
+let rec subst_pat_iterator y t = function
+  | PatVar (_,id) as x ->
+      if id = Name y then t else x
+  | PatCstr (loc,id,l,alias) ->
+      PatCstr (loc,id,List.map (subst_pat_iterator y t) l,alias)
+
+let subst_cases_pattern loc aliases intern subst scopes a =
+  let rec aux aliases subst = function
+  | AVar id ->
+      begin
+	(* subst remembers the delimiters stack in the interpretation *)
+	(* of the notations *)
+	try 
+	  let (a,(scopt,subscopes)) = List.assoc id subst in
+	  intern (subscopes@scopes) ([],[]) scopt a
+	with Not_found -> 
+	  if id = ldots_var then [[],[]], PatVar (loc,Name id) else
+	  anomaly ("Unbound pattern notation variable: "^(string_of_id id))
+	  (*
+	  (* Happens for local notation joint with inductive/fixpoint defs *)
+	  if aliases <> ([],[]) then
+	    anomaly "Pattern notation without constructors";
+	  [[id],[]], PatVar (loc,Name id)
+	  *)
+      end
+  | ARef (ConstructRef c) ->
+      [aliases], PatCstr (loc,c, [], alias_of aliases)
+  | AApp (ARef (ConstructRef (ind,_ as c)),args) ->
+      let nparams = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in
+      let _,args = list_chop nparams args in
+      let (idsl,pl) = List.split (List.map (aux ([],[]) subst) args) in
+      aliases::List.flatten idsl, PatCstr (loc,c,pl,alias_of aliases)
+  | AList (x,_,iter,terminator,lassoc) ->
+      (try 
+        (* All elements of the list are in scopes (scopt,subscopes) *)
+	let (a,(scopt,subscopes)) = List.assoc x subst in
+        let idslt,termin = aux ([],[]) subst terminator in
+        let l = decode_patlist_value a in
+        let idsl,v =
+	  List.fold_right (fun a (allidsl,t) -> 
+            let idsl,u = aux ([],[]) ((x,(a,(scopt,subscopes)))::subst) iter in
+            idsl::allidsl, subst_pat_iterator ldots_var t u)
+            (if lassoc then List.rev l else l) ([idslt],termin) in
+        aliases::List.flatten idsl, v
+      with Not_found -> 
+          anomaly "Inconsistent substitution of recursive notation")
+  | t -> user_err_loc (loc,"",str "Invalid notation for pattern")
+  in aux aliases subst a
+
+(* Differentiating between constructors and matching variables *)
+type pattern_qualid_kind =
+  | ConstrPat of (constructor * cases_pattern list)
+  | VarPat of identifier
+
+let rec patt_of_rawterm loc cstr =
+  match cstr with
+    | RRef (_,(ConstructRef c as x)) ->
+	if !dump then add_glob loc x; 
+ 	(c,[])
+    | RApp (_,RApp(_,h,l1),l2) -> patt_of_rawterm loc (RApp(loc,h,l1@l2))
+    | RApp (_,RRef(_,(ConstructRef c as x)),pl) ->
+        if !dump then add_glob loc x;
+        let (_,mib) = Inductive.lookup_mind_specif (Global.env()) (fst c) in
+        let npar = mib.Declarations.mind_nparams in
+        let (params,args) =
+          if List.length pl <= npar then (pl,[]) else
+            list_chop npar pl in
+        (* All parameters must be _ *)
+        List.iter
+          (function RHole _ -> ()
+            | _ -> raise Not_found) params;
+        let pl' = List.map
+          (fun c ->
+            let (c,pl) = patt_of_rawterm loc c in
+            PatCstr(loc,c,pl,Anonymous)) args in
+        (c,pl')
+    | _ -> raise Not_found
+
+let find_constructor ref =
+  let (loc,qid) = qualid_of_reference ref in
+  let gref =
+    try extended_locate qid
+    with Not_found ->
+      raise (InternalisationError (loc,NotAConstructor ref)) in
+  match gref with
+    | SyntacticDef sp ->
+        let sdef = Syntax_def.search_syntactic_definition loc sp in
+        patt_of_rawterm loc sdef
+    | TrueGlobal r ->
+        let rec unf = function
+          | ConstRef cst ->
+	      let v = Environ.constant_value (Global.env()) cst in
+              unf (reference_of_constr v)
+          | ConstructRef c -> 
+	      if !dump then add_glob loc r; 
+	      c, []
+          | _ -> raise Not_found
+        in unf r
+
+let find_pattern_variable = function
+  | Ident (loc,id) -> id
+  | Qualid (loc,_) as x -> raise (InternalisationError(loc,NotAConstructor x))
+
+let maybe_constructor ref =
+  try ConstrPat (find_constructor ref)
+  with
+      (* patt var does not exists globally *)
+    | InternalisationError _ -> VarPat (find_pattern_variable ref)
+      (* patt var also exists globally but does not satisfy preconditions *)
+    | (Environ.NotEvaluableConst _ | Not_found) ->
+        warn (str "pattern " ++ pr_reference ref ++
+              str " is understood as a pattern variable");
+        VarPat (find_pattern_variable ref)
+
+let mustbe_constructor loc ref = 
+  try find_constructor ref
+  with (Environ.NotEvaluableConst _ | Not_found) ->
+    raise (InternalisationError (loc,NotAConstructor ref))
+
+let rec intern_cases_pattern scopes aliases tmp_scope = function
+  | CPatAlias (loc, p, id) ->
+      let aliases' = merge_aliases aliases id in
+      intern_cases_pattern scopes aliases' tmp_scope p
+  | CPatCstr (loc, head, pl) ->
+      let c,pl0 = mustbe_constructor loc head in
+      let argscs =
+	simple_adjust_scopes (find_arguments_scope (ConstructRef c), pl) in
+      let (idsl,pl') =
+	List.split (List.map2 (intern_cases_pattern scopes ([],[])) argscs pl)
+      in
+      (aliases::(List.flatten idsl), PatCstr (loc,c,pl0@pl',alias_of aliases))
+  | CPatNotation (loc,"- _",[CPatNumeral(_,Bignat.POS p)]) ->
+      let scopes = option_cons tmp_scope scopes in
+      ([aliases],
+      Symbols.interp_numeral_as_pattern loc (Bignat.NEG p)
+        (alias_of aliases) scopes)
+  | CPatNotation (_,"( _ )",[a]) ->
+      intern_cases_pattern scopes aliases tmp_scope a
+  | CPatNotation (loc, ntn, args) ->
+      let ntn,args = contract_pat_notation ntn args in
+      let scopes = option_cons tmp_scope scopes in
+      let ((ids,c),df) = Symbols.interp_notation loc ntn scopes in
+      if !dump then dump_notation_location (patntn_loc loc args ntn) ntn df;
+      let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
+      subst_cases_pattern loc aliases intern_cases_pattern subst scopes c
+  | CPatNumeral (loc, n) ->
+      let scopes = option_cons tmp_scope scopes in
+      ([aliases],
+      Symbols.interp_numeral_as_pattern loc n (alias_of aliases) scopes)
+  | CPatDelimiters (loc, key, e) ->
+      intern_cases_pattern (find_delimiters_scope loc key::scopes)
+        aliases None e
+  | CPatAtom (loc, Some head) ->
+      (match maybe_constructor head with
+	 | ConstrPat (c,args) ->
+	     ([aliases], PatCstr (loc,c,args,alias_of aliases))
+	 | VarPat id ->
+	     let aliases = merge_aliases aliases id in
+	     ([aliases], PatVar (loc,alias_of aliases)))
+  | CPatAtom (loc, None) ->
+      ([aliases], PatVar (loc,alias_of aliases))
+
+(**********************************************************************)
+(* Fix and CoFix                                                      *)
+
+(**********************************************************************)
+(* Utilities for binders                                              *)
+
+let check_capture loc ty = function
+  | Name id when occur_var_constr_expr id ty ->
+      raise (InternalisationError (loc,VariableCapture id))
+  | _ ->
+      ()
+
+let locate_if_isevar loc na = function
+  | RHole _ -> 
+      (try match na with
+	| Name id ->  Reserve.find_reserved_type id
+	| Anonymous -> raise Not_found 
+      with Not_found -> RHole (loc, BinderType na))
+  | x -> x
+
+let check_hidden_implicit_parameters id (_,_,_,indnames,_) =
+  if List.mem id indnames then
+    errorlabstrm "" (str "A parameter or name of an inductive type " ++
+    pr_id id ++ str " must not be used as a bound variable in the type \
+of its constructor")
+
+let push_name_env lvar (ids,tmpsc,scopes as env) = function
+  | Anonymous -> env 
+  | Name id -> 
+      check_hidden_implicit_parameters id lvar;
+      (Idset.add id ids,tmpsc,scopes)
+
+(**********************************************************************)
+(* Utilities for application                                          *)
+
+let merge_impargs l args =
+  List.fold_right (fun a l ->
+    match a with 
+      | (_,Some (_,(ExplByName id as x))) when 
+	  List.exists (function (_,Some (_,y)) -> x=y | _ -> false) args -> l
+      | _ -> a::l)
+    l args 
+
+let check_projection isproj nargs r = 
+  match (r,isproj) with
+  | RRef (loc, ref), Some nth ->
+      (try
+	let n = Recordops.find_projection_nparams ref in
+	if nargs < nth then 
+	  user_err_loc (loc,"",str "Projection has not enough parameters");
+      with Not_found -> 
+	user_err_loc
+	(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection"))
+  | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection")
+  | _, None -> ()
+
+let set_hole_implicit i = function
+  | RRef (loc,r) -> (loc,ImplicitArg (r,i))
+  | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i))
+  | _ -> anomaly "Only refs have implicits"
+
+let exists_implicit_name id =
+  List.exists (fun imp -> is_status_implicit imp & id = name_of_implicit imp)
+
+let extract_explicit_arg imps args =
+  let rec aux = function
+  | [] -> [],[]
+  | (a,e)::l ->
+      let (eargs,rargs) = aux l in
+      match e with
+      | None -> (eargs,a::rargs)
+      | Some (loc,pos) ->
+	  let id = match pos with
+	  | ExplByName id ->
+	      if not (exists_implicit_name id imps) then
+		user_err_loc (loc,"",str "Wrong argument name: " ++ pr_id id);
+	      if List.mem_assoc id eargs then
+		user_err_loc (loc,"",str "Argument name " ++ pr_id id
+		++ str " occurs more than once");
+	      id
+	  | ExplByPos p ->
+	      let id =
+		try 
+		  let imp = List.nth imps (p-1) in
+		  if not (is_status_implicit imp) then failwith "imp";
+		  name_of_implicit imp
+		with Failure _ (* "nth" | "imp" *) ->
+		  user_err_loc (loc,"",str"Wrong argument position: " ++ int p)
+	      in
+	      if List.mem_assoc id eargs then
+		user_err_loc (loc,"",str"Argument at position " ++ int p ++
+		  str " is mentioned more than once");
+	      id in
+	  ((id,(loc,a))::eargs,rargs)
+  in aux args
+
+(**********************************************************************)
+(* Syntax extensions                                                  *)
+
+let coerce_to_id = function
+  | CRef (Ident (_,id)) -> id 
+  | c ->
+      user_err_loc (constr_loc c, "subst_rawconstr",
+        str"This expression should be a simple identifier")
+
+let traverse_binder subst id (ids,tmpsc,scopes as env) =
+  let id = try coerce_to_id (fst (List.assoc id subst)) with Not_found -> id in
+  id,(Idset.add id ids,tmpsc,scopes)
+
+let decode_constrlist_value = function
+  | CAppExpl (_,_,l) -> l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
+let rec subst_iterator y t = function
+  | RVar (_,id) as x -> if id = y then t else x
+  | x -> map_rawconstr (subst_iterator y t) x
+
+let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as env) =
+  function
+  | AVar id ->
+      begin
+	(* subst remembers the delimiters stack in the interpretation *)
+	(* of the notations *)
+	try 
+	  let (a,(scopt,subscopes)) = List.assoc id subst in
+	  interp (ids,scopt,subscopes@scopes) a
+	with Not_found -> 
+	  (* Happens for local notation joint with inductive/fixpoint defs *)
+	  RVar (loc,id)
+      end
+  | AList (x,_,iter,terminator,lassoc) ->
+      (try 
+        (* All elements of the list are in scopes (scopt,subscopes) *)
+	let (a,(scopt,subscopes)) = List.assoc x subst in
+        let termin = 
+          subst_aconstr_in_rawconstr loc interp subst (ids,None,scopes) 
+            terminator in
+        let l = decode_constrlist_value a in
+	List.fold_right (fun a t -> 
+          subst_iterator ldots_var t
+            (subst_aconstr_in_rawconstr loc interp 
+              ((x,(a,(scopt,subscopes)))::subst)
+              (ids,None,scopes) iter))
+            (if lassoc then List.rev l else l) termin
+      with Not_found -> 
+          anomaly "Inconsistent substitution of recursive notation")
+  | t ->
+      rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
+      (subst_aconstr_in_rawconstr loc interp subst) (ids,None,scopes) t
+
+let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
+  let ntn,args = contract_notation ntn args in
+  let scopes = option_cons tmp_scope scopes in
+  let ((ids,c),df) = Symbols.interp_notation loc ntn scopes in
+  if !dump then dump_notation_location (ntn_loc loc args ntn) ntn df;
+  let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
+  subst_aconstr_in_rawconstr loc intern subst env c
+
+let set_type_scope (ids,tmp_scope,scopes) =
+  (ids,Some Symbols.type_scope,scopes)
+
+let reset_tmp_scope (ids,tmp_scope,scopes) =
+  (ids,None,scopes)
+
+(**********************************************************************)
+(* Main loop                                                          *)
+
+let internalise sigma env allow_soapp lvar c =
+  let rec intern (ids,tmp_scope,scopes as env) = function
+    | CRef ref as x ->
+	let (c,imp,subscopes,l) = intern_reference env lvar ref in
+	(match intern_impargs c env imp subscopes l with
+          | [] -> c
+          | l -> RApp (constr_loc x, c, l))
+    | CFix (loc, (locid,iddef), dl) ->
+        let lf = List.map (fun (id,_,_,_,_) -> id) dl in
+        let dl = Array.of_list dl in
+	let n =
+	  try
+	    (list_index iddef lf) -1
+          with Not_found ->
+	    raise (InternalisationError (locid,UnboundFixName (false,iddef)))
+	in
+	let ids' = List.fold_right Idset.add lf ids in
+        let idl = Array.map
+          (fun (id,n,bl,ty,bd) ->
+            let ((ids'',_,_),rbl) =
+              List.fold_left intern_local_binder (env,[]) bl in
+	    let ids''' = List.fold_right Idset.add lf ids'' in
+            (List.rev rbl,
+             intern_type (ids'',tmp_scope,scopes) ty,
+             intern (ids''',None,scopes) bd)) dl in
+	RRec (loc,RFix (Array.map (fun (_,n,_,_,_) -> n) dl,n),
+              Array.of_list lf,
+              Array.map (fun (bl,_,_) -> bl) idl,
+              Array.map (fun (_,ty,_) -> ty) idl,
+              Array.map (fun (_,_,bd) -> bd) idl)
+    | CCoFix (loc, (locid,iddef), dl) ->
+        let lf = List.map (fun (id,_,_,_) -> id) dl in
+        let dl = Array.of_list dl in
+	let n =
+          try 
+	    (list_index iddef lf) -1
+          with Not_found ->
+	    raise (InternalisationError (locid,UnboundFixName (true,iddef)))
+	in
+	let ids' = List.fold_right Idset.add lf ids in
+        let idl = Array.map
+          (fun (id,bl,ty,bd) ->
+            let ((ids'',_,_),rbl) =
+              List.fold_left intern_local_binder (env,[]) bl in
+	    let ids''' = List.fold_right Idset.add lf ids'' in
+            (List.rev rbl,
+             intern_type (ids'',tmp_scope,scopes) ty,
+             intern (ids''',None,scopes) bd)) dl in
+	RRec (loc,RCoFix n,
+              Array.of_list lf,
+              Array.map (fun (bl,_,_) -> bl) idl,
+              Array.map (fun (_,ty,_) -> ty) idl,
+              Array.map (fun (_,_,bd) -> bd) idl)
+    | CArrow (loc,c1,c2) ->
+        RProd (loc, Anonymous, intern_type env c1, intern_type env c2)
+    | CProdN (loc,[],c2) ->
+        intern_type env c2
+    | CProdN (loc,(nal,ty)::bll,c2) ->
+        iterate_prod loc env ty (CProdN (loc, bll, c2)) nal
+    | CLambdaN (loc,[],c2) ->
+        intern env c2
+    | CLambdaN (loc,(nal,ty)::bll,c2) ->
+	iterate_lam loc (reset_tmp_scope env) ty (CLambdaN (loc, bll, c2)) nal
+    | CLetIn (loc,(_,na),c1,c2) ->
+	RLetIn (loc, na, intern (reset_tmp_scope env) c1,
+          intern (push_name_env lvar env na) c2)
+    | CNotation (loc,"- _",[CNumeral(_,Bignat.POS p)]) ->
+        let scopes = option_cons tmp_scope scopes in
+        Symbols.interp_numeral loc (Bignat.NEG p) scopes
+    | CNotation (_,"( _ )",[a]) -> intern env a
+    | CNotation (loc,ntn,args) ->
+        intern_notation intern env loc ntn args
+    | CNumeral (loc, n) ->
+	let scopes = option_cons tmp_scope scopes in
+	Symbols.interp_numeral loc n scopes
+    | CDelimiters (loc, key, e) ->
+	intern (ids,None,find_delimiters_scope loc key::scopes) e
+    | CAppExpl (loc, (isproj,ref), args) ->
+        let (f,_,args_scopes,_) = intern_reference env lvar ref in
+	check_projection isproj (List.length args) f;
+	RApp (loc, f, intern_args env args_scopes args)
+    | CApp (loc, (isproj,f), args) ->
+        let isproj,f,args = match f with
+          (* Compact notations like "t.(f args') args" *)
+          | CApp (_,(Some _,f), args') when isproj=None -> isproj,f,args'@args
+          (* Don't compact "(f args') args" to resolve implicits separately *)
+          | _ -> isproj,f,args in
+	let (c,impargs,args_scopes,l) =
+          match f with
+            | CRef ref -> intern_reference env lvar ref
+            | CNotation (loc,ntn,[]) ->
+                let c = intern_notation intern env loc ntn [] in
+                find_appl_head_data lvar c
+            | x -> (intern env f,[],[],[]) in
+	let args = intern_impargs c env impargs args_scopes (merge_impargs l args) in
+	check_projection isproj (List.length args) c;
+	(match c with 
+          (* Now compact "(f args') args" *)
+	  | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
+	  | _ -> RApp (loc, c, args))
+    | CCases (loc, (po,rtnpo), tms, eqns) ->
+        let tms,env' = List.fold_right
+          (fun citm (inds,env) ->
+	    let (tm,ind),nal = intern_case_item env citm in
+	    (tm,ref ind)::inds,List.fold_left (push_name_env lvar) env nal)
+	  tms ([],env) in
+        let rtnpo = option_app (intern_type env') rtnpo in
+	RCases (loc, (option_app (intern_type env) po, ref rtnpo), tms,
+		List.map (intern_eqn (List.length tms) env) eqns)
+    | COrderedCase (loc, tag, po, c, cl) ->
+	let env = reset_tmp_scope env in
+	ROrderedCase (loc, tag, option_app (intern_type env) po,
+	          intern env c,
+		  Array.of_list (List.map (intern env) cl),ref None)
+    | CLetTuple (loc, nal, (na,po), b, c) ->
+	let env' = reset_tmp_scope env in
+        let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
+        let env'' = List.fold_left (push_name_env lvar) env ids in
+        let p' = option_app (intern_type env'') po in
+        RLetTuple (loc, nal, (na', p'), b',
+                   intern (List.fold_left (push_name_env lvar) env nal) c)
+    | CIf (loc, c, (na,po), b1, b2) ->
+	let env' = reset_tmp_scope env in
+        let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
+        let env'' = List.fold_left (push_name_env lvar) env ids in
+        let p' = option_app (intern_type env'') po in
+        RIf (loc, c', (na', p'), intern env b1, intern env b2)
+    | CHole loc -> 
+	RHole (loc, QuestionMark)
+    | CPatVar (loc, n) when allow_soapp ->
+	RPatVar (loc, n)
+    | CPatVar (loc, (false,n)) when Options.do_translate () ->
+	RVar (loc, n)
+    | CPatVar (loc, (false,n as x)) ->
+        if List.mem n (fst (let (a,_,_,_,_) = lvar in a)) & !Options.v7 then
+	  RVar (loc, n)
+	else
+          error_unbound_patvar loc n
+    | CPatVar (loc, _) ->
+	raise (InternalisationError (loc,NegativeMetavariable))
+    | CEvar (loc, n) ->
+	REvar (loc, n, None)
+    | CSort (loc, s) ->
+	RSort(loc,s)
+    | CCast (loc, c1, c2) ->
+	RCast (loc,intern env c1,intern_type env c2)
+
+    | CDynamic (loc,d) -> RDynamic (loc,d)
+
+  and intern_type (ids,_,scopes) =
+    intern (ids,Some Symbols.type_scope,scopes)
+
+  and intern_local_binder ((ids,ts,sc as env),bl) = function
+      LocalRawAssum(nal,ty) ->
+        let ty = intern_type env ty in
+        List.fold_left
+          (fun ((ids,ts,sc),bl) (_,na) ->
+            ((name_fold Idset.add na ids,ts,sc), (na,None,ty)::bl))
+          (env,bl) nal
+    | LocalRawDef((loc,na),def) ->
+        ((name_fold Idset.add na ids,ts,sc),
+         (na,Some(intern env def),RHole(loc,BinderType na))::bl)
+
+  and intern_eqn n (ids,tmp_scope,scopes as env) (loc,lhs,rhs) =
+	let (idsl_substl_list,pl) =
+	  List.split 
+	    (List.map (intern_cases_pattern scopes ([],[]) None) lhs) in
+	let idsl, substl = List.split (List.flatten idsl_substl_list) in
+	let eqn_ids = List.flatten idsl in
+	let subst = List.flatten substl in 
+	(* Linearity implies the order in ids is irrelevant *)
+	check_linearity lhs eqn_ids;
+	check_uppercase loc eqn_ids;
+	check_number_of_pattern loc n pl;
+	let rhs = replace_vars_constr_expr subst rhs in
+	List.iter message_redundant_alias subst;
+	let env_ids = List.fold_right Idset.add eqn_ids ids in
+	(loc, eqn_ids,pl,intern (env_ids,tmp_scope,scopes) rhs)
+
+  and intern_case_item (vars,_,scopes as env) (tm,(na,t)) =
+    let tm' = intern env tm in
+    let ids,typ = match t with
+    | Some t -> 
+	let tids = names_of_cases_indtype t in
+	let tids = List.fold_right Idset.add tids Idset.empty in
+	let t = intern_type (tids,None,scopes) t in
+	begin match t with
+	  | RRef (loc,IndRef ind) -> [],Some (loc,ind,[])
+	  | RApp (loc,RRef (_,IndRef ind),l) ->
+	      let nal = List.map (function
+		| RHole _ -> Anonymous
+		| RVar (_,id) -> Name id
+		| c ->
+		    user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in
+	      nal, Some (loc,ind,nal)
+	  | _ -> error_bad_inductive_type (loc_of_rawconstr t)
+	end
+    | None -> 
+	[], None in
+    let na = match tm', na with
+      | RVar (_,id), None when Idset.mem id vars & not !Options.v7 -> Name id
+      | _, None -> Anonymous
+      | _, Some na -> na in
+    (tm',(na,typ)), na::ids
+
+  and iterate_prod loc2 env ty body = function
+    | (loc1,na)::nal ->
+	if nal <> [] then check_capture loc1 ty na;
+	let body = iterate_prod loc2 (push_name_env lvar env na) ty body nal in
+	let ty = locate_if_isevar loc1 na (intern_type env ty) in
+	RProd (join_loc loc1 loc2, na, ty, body)
+    | [] -> intern_type env body
+
+  and iterate_lam loc2 env ty body = function
+    | (loc1,na)::nal ->
+	if nal <> [] then check_capture loc1 ty na;
+	let body = iterate_lam loc2 (push_name_env lvar env na) ty body nal in
+	let ty = locate_if_isevar loc1 na (intern_type env ty) in
+	RLambda (join_loc loc1 loc2, na, ty, body)
+    | [] -> intern env body
+
+  and intern_impargs c env l subscopes args =
+    let eargs, rargs = extract_explicit_arg l args in
+    let rec aux n impl subscopes eargs rargs =
+      let (enva,subscopes') = apply_scope_env env subscopes in
+      match (impl,rargs) with
+      | (imp::impl', rargs) when is_status_implicit imp ->
+	  begin try 
+	    let id = name_of_implicit imp in
+	    let (_,a) = List.assoc id eargs in
+	    let eargs' = List.remove_assoc id eargs in
+	    intern enva a :: aux (n+1) impl' subscopes' eargs' rargs
+	  with Not_found ->
+	  if rargs=[] & eargs=[] &
+	    not (List.for_all is_status_implicit impl') then
+	    (* Less regular arguments than expected: don't complete *)
+	    (* with implicit arguments *)
+	    []
+	  else
+	    RHole (set_hole_implicit n c) :: 
+	      aux (n+1) impl' subscopes' eargs rargs
+	  end
+      | (imp::impl', a::rargs') ->
+	  intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
+      | (imp::impl', []) -> 
+	  if eargs <> [] then 
+	    (let (id,(loc,_)) = List.hd eargs in
+	    user_err_loc (loc,"",str "Not enough non implicit
+	    arguments to accept the argument bound to " ++ pr_id id));
+	  []
+      | ([], rargs) ->
+	  assert (eargs = []);
+	  intern_args env subscopes rargs
+    in aux 1 l subscopes eargs rargs
+
+  and intern_args env subscopes = function
+    | [] -> []
+    | a::args ->
+        let (enva,subscopes) = apply_scope_env env subscopes in
+        (intern enva a) :: (intern_args env subscopes args)
+
+  in 
+  try 
+    intern env c
+  with
+      InternalisationError (loc,e) ->
+	user_err_loc (loc,"internalize",explain_internalisation_error e)
+
+(**************************************************************************)
+(* Functions to translate constr_expr into rawconstr                       *)
+(**************************************************************************)
+
+let extract_ids env =
+  List.fold_right Idset.add 
+    (Termops.ids_of_rel_context (Environ.rel_context env))
+    Idset.empty
+
+let interp_rawconstr_gen_with_implicits isarity sigma env (indpars,impls) allow_soapp ltacvar c =
+  let tmp_scope = if isarity then Some Symbols.type_scope else None in
+  internalise sigma (extract_ids env, tmp_scope,[])
+    allow_soapp (ltacvar,Environ.named_context env, [], indpars, impls) c
+
+let interp_rawconstr_gen isarity sigma env allow_soapp ltacvar c =
+  interp_rawconstr_gen_with_implicits isarity sigma env ([],[]) allow_soapp ltacvar c
+
+let interp_rawconstr sigma env c =
+  interp_rawconstr_gen false sigma env false ([],[]) c
+
+let interp_rawtype sigma env c =
+  interp_rawconstr_gen true sigma env false ([],[]) c
+
+let interp_rawtype_with_implicits sigma env impls c =
+  interp_rawconstr_gen_with_implicits true sigma env impls false ([],[]) c
+
+let interp_rawconstr_with_implicits sigma env vars impls c =
+  interp_rawconstr_gen_with_implicits false sigma env ([],impls) false
+    (vars,[]) c
+
+(*
+(* The same as interp_rawconstr but with a list of variables which must not be
+   globalized *)
+
+let interp_rawconstr_wo_glob sigma env lvar c =
+  interp_rawconstr_gen sigma env [] (Some []) lvar c
+*)
+
+(*********************************************************************)
+(* Functions to parse and interpret constructions *)
+
+let interp_constr sigma env c =
+  understand sigma env (interp_rawconstr sigma env c)
+
+let interp_openconstr sigma env c =
+  understand_gen_tcc sigma env [] None (interp_rawconstr sigma env c)
+
+let interp_casted_openconstr sigma env c typ =
+  understand_gen_tcc sigma env [] (Some typ) (interp_rawconstr sigma env c)
+
+let interp_type sigma env c =
+  understand_type sigma env (interp_rawtype sigma env c)
+
+let interp_binder sigma env na t =
+  let t = interp_rawtype sigma env t in
+  understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t)
+
+let interp_type_with_implicits sigma env impls c =
+  understand_type sigma env (interp_rawtype_with_implicits sigma env impls c)
+
+let judgment_of_rawconstr sigma env c =
+  understand_judgment sigma env (interp_rawconstr sigma env c)
+
+let type_judgment_of_rawconstr sigma env c =
+  understand_type_judgment sigma env (interp_rawconstr sigma env c)
+
+(* To retype a list of key*constr with undefined key *)
+let retype_list sigma env lst =
+  List.fold_right (fun (x,csr) a ->
+    try (x,Retyping.get_judgment_of env sigma csr)::a with
+    | Anomaly _ -> a) lst []
+
+(*  List.map (fun (x,csr) -> (x,Retyping.get_judgment_of env sigma csr)) lst*)
+
+type ltac_sign = 
+  identifier list * (identifier * identifier option) list
+
+type ltac_env = 
+  (identifier * Term.constr) list * (identifier * identifier option) list
+
+(* Interprets a constr according to two lists *)
+(* of instantiations (variables and metas)    *)
+(* Note: typ is retyped *)
+let interp_constr_gen sigma env (ltacvars,unbndltacvars) c exptyp =
+  let c = interp_rawconstr_gen false sigma env false
+    (List.map fst ltacvars,unbndltacvars) c in
+  let typs = retype_list sigma env ltacvars in
+  understand_gen sigma env typs exptyp c
+
+(*Interprets a casted constr according to two lists of instantiations
+  (variables and metas)*)
+let interp_openconstr_gen sigma env (ltacvars,unbndltacvars) c exptyp =
+  let c = interp_rawconstr_gen false sigma env false
+    (List.map fst ltacvars,unbndltacvars) c in
+  let typs = retype_list sigma env ltacvars in
+  understand_gen_tcc sigma env typs exptyp c
+
+let interp_casted_constr sigma env c typ = 
+  understand_gen sigma env [] (Some typ) (interp_rawconstr sigma env c)
+
+let interp_casted_constr_with_implicits sigma env impls c typ =
+  understand_gen sigma env [] (Some typ) 
+    (interp_rawconstr_with_implicits sigma env [] impls c)
+
+let interp_constrpattern_gen sigma env ltacvar c =
+  let c = interp_rawconstr_gen false sigma env true (ltacvar,[]) c in
+  pattern_of_rawconstr c
+
+let interp_constrpattern sigma env c =
+  interp_constrpattern_gen sigma env [] c
+
+let interp_aconstr impls vars a =
+  let env = Global.env () in
+  (* [vl] is intended to remember the scope of the free variables of [a] *)
+  let vl = List.map (fun id -> (id,ref None)) vars in
+  let c = internalise Evd.empty (extract_ids env, None, [])
+    false (([],[]),Environ.named_context env,vl,[],impls) a in
+  (* Translate and check that [c] has all its free variables bound in [vars] *)
+  let a = aconstr_of_rawconstr vars c in
+  (* Returns [a] and the ordered list of variables with their scopes *)
+  (* Variables occurring in binders have no relevant scope since bound *)
+  List.map
+    (fun (id,r) -> (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl,
+  a
+
+(**********************************************************************)
+(* Locating reference, possibly via an abbreviation *)
+
+let locate_reference qid =
+  match Nametab.extended_locate qid with
+    | TrueGlobal ref -> ref
+    | SyntacticDef kn -> 
+	match Syntax_def.search_syntactic_definition dummy_loc kn with
+	  | Rawterm.RRef (_,ref) -> ref
+	  | _ -> raise Not_found
+
+let is_global id =
+  try 
+    let _ = locate_reference (make_short_qualid id) in true
+  with Not_found -> 
+    false
+
+let global_reference id = 
+  constr_of_reference (locate_reference (make_short_qualid id))
+
+let construct_reference ctx id =
+  try
+    Term.mkVar (let _ = Sign.lookup_named id ctx in id)
+  with Not_found ->
+    global_reference id
+
+let global_reference_in_absolute_module dir id = 
+  constr_of_reference (Nametab.absolute_reference (Libnames.make_path dir id))
+
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
new file mode 100644
index 00000000..a65ab6a7
--- /dev/null
+++ b/interp/constrintern.mli
@@ -0,0 +1,126 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: constrintern.mli,v 1.15.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+
+(*i*)
+open Names
+open Term
+open Sign
+open Evd
+open Environ
+open Libnames
+open Rawterm
+open Pattern
+open Coqast
+open Topconstr
+open Termops
+(*i*)
+
+(*s Translation from front abstract syntax of term to untyped terms (rawconstr)
+
+   The translation performs:
+
+   - resolution of names :
+      - check all variables are bound
+      - make absolute the references to global objets
+   - resolution of symbolic notations using scopes
+   - insert existential variables for implicit arguments
+*)
+
+(* To interpret implicits and arg scopes of recursive variables in
+   inductive types and recursive definitions *)
+type var_internalisation_data =
+    identifier list * Impargs.implicits_list * scope_name option list
+
+type implicits_env = (identifier * var_internalisation_data) list
+type full_implicits_env = identifier list * implicits_env
+
+type ltac_sign = 
+  identifier list * (identifier * identifier option) list
+
+type ltac_env = 
+  (identifier * constr) list * (identifier * identifier option) list
+
+(* Interprets global names, including syntactic defs and section variables *)
+val interp_rawconstr     : evar_map -> env -> constr_expr -> rawconstr
+val interp_rawconstr_gen : bool -> evar_map -> env -> 
+    bool -> ltac_sign -> constr_expr -> rawconstr
+
+(*s Composing the translation with typing *)
+val interp_constr        : evar_map -> env -> constr_expr -> constr
+val interp_casted_constr : evar_map -> env -> constr_expr -> types -> constr
+val interp_type          : evar_map -> env -> constr_expr -> types
+val interp_binder        : evar_map -> env -> name -> constr_expr -> types
+val interp_openconstr    : evar_map -> env -> constr_expr -> evar_map * constr
+val interp_casted_openconstr    :
+  evar_map -> env -> constr_expr -> constr -> evar_map * constr
+
+(* [interp_type_with_implicits] extends [interp_type] by allowing
+   implicits arguments in the ``rel'' part of [env]; the extra
+   argument associates a list of implicit positions to identifiers
+   declared in the rel_context of [env] *)
+val interp_type_with_implicits : 
+  evar_map -> env -> full_implicits_env -> constr_expr -> types
+
+val interp_casted_constr_with_implicits :
+  evar_map -> env -> implicits_env -> constr_expr -> types -> constr
+
+val interp_rawconstr_with_implicits :
+  evar_map -> env -> identifier list -> implicits_env -> constr_expr -> 
+    rawconstr
+
+(*s Build a judgement from *)
+val judgment_of_rawconstr : evar_map -> env -> constr_expr -> unsafe_judgment
+val type_judgment_of_rawconstr :
+  evar_map -> env -> constr_expr -> unsafe_type_judgment
+
+(* Interprets a constr according to two lists of instantiations (variables and
+  metas), possibly casting it*)
+val interp_constr_gen     :
+  evar_map -> env -> ltac_env -> constr_expr -> constr option -> constr
+
+(* Interprets a constr according to two lists of instantiations (variables and
+  metas), possibly casting it, and turning unresolved evar into metas*)
+val interp_openconstr_gen     :
+  evar_map -> env -> ltac_env ->
+    constr_expr -> constr option -> evar_map * constr
+
+(* Interprets constr patterns according to a list of instantiations
+  (variables)*)
+val interp_constrpattern_gen : evar_map -> env -> identifier list ->
+  constr_expr -> patvar list * constr_pattern
+
+val interp_constrpattern : 
+  evar_map -> env -> constr_expr -> patvar list * constr_pattern
+
+val interp_reference : ltac_sign -> reference -> rawconstr
+
+(* Locating references of constructions, possibly via a syntactic definition *)
+
+val locate_reference : qualid -> global_reference
+val is_global : identifier -> bool
+val construct_reference : named_context -> identifier -> constr
+val global_reference : identifier -> constr
+val global_reference_in_absolute_module : dir_path -> identifier -> constr
+
+(* Interprets into a abbreviatable constr *)
+val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
+  interpretation
+
+(* Globalization leak for Grammar *)
+val for_grammar : ('a -> 'b) -> 'a -> 'b
+
+(* Coqdoc utility functions *)
+type coqdoc_state
+val coqdoc_freeze : unit -> coqdoc_state
+val coqdoc_unfreeze : coqdoc_state -> unit
+
+(* For v8 translation *)
+val set_temporary_implicits_in :
+  (identifier * Impargs.implicits_list) list -> unit
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
new file mode 100644
index 00000000..8ce9bfaf
--- /dev/null
+++ b/interp/coqlib.ml
@@ -0,0 +1,294 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: coqlib.ml,v 1.14.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+
+open Util
+open Pp
+open Names
+open Term
+open Libnames
+open Pattern
+open Nametab
+
+let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+
+let gen_reference locstr dir s =
+  let dir = make_dir ("Coq"::dir) in
+  let id = Constrextern.id_of_v7_string s in
+  let sp = Libnames.make_path dir id in
+  try
+    Nametab.absolute_reference sp
+  with Not_found ->
+    anomaly (locstr^": cannot find "^(string_of_path sp))
+    
+let gen_constant locstr dir s = 
+  constr_of_reference (gen_reference locstr dir s)
+
+let list_try_find f = 
+  let rec try_find_f = function
+    | [] -> raise Not_found
+    | h::t -> try f h with Not_found -> try_find_f t
+  in 
+  try_find_f
+
+let has_suffix_in_dirs dirs ref =
+  let dir = dirpath (sp_of_global ref) in
+  List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
+
+let gen_constant_in_modules locstr dirs s =
+  let dirs = List.map make_dir dirs in
+  let id = Constrextern.id_of_v7_string s in
+  let all = Nametab.locate_all (make_short_qualid id) in
+  let these = List.filter (has_suffix_in_dirs dirs) all in
+  match these with
+    | [x] -> constr_of_reference x
+    | [] ->
+	anomalylabstrm "" (str (locstr^": cannot find "^s^
+	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
+	prlist_with_sep pr_coma pr_dirpath dirs)
+    | l ->
+	anomalylabstrm "" 
+	(str (locstr^": found more than once object of name "^s^
+	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
+	prlist_with_sep pr_coma pr_dirpath dirs)
+
+let init_reference dir s=gen_reference "Coqlib" ("Init"::dir) s
+
+let init_constant dir s=gen_constant "Coqlib" ("Init"::dir) s  
+
+let arith_dir = ["Coq";"Arith"]
+let arith_modules = [arith_dir]
+
+let narith_dir = ["Coq";"NArith"]
+
+let zarith_dir = ["Coq";"ZArith"]
+let zarith_base_modules = [narith_dir;zarith_dir]
+
+let init_dir = ["Coq";"Init"]
+let init_modules = [
+  init_dir@["Datatypes"];
+  init_dir@["Logic"];
+  init_dir@["Specif"];
+  init_dir@["Logic_Type"];
+  init_dir@["Peano"];
+  init_dir@["Wf"]
+]
+  
+let coq_id = id_of_string "Coq"
+let init_id = id_of_string "Init"
+let arith_id = id_of_string "Arith"
+let datatypes_id = id_of_string "Datatypes"
+
+let logic_module = make_dir ["Coq";"Init";"Logic"]
+let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"]
+let datatypes_module = make_dir ["Coq";"Init";"Datatypes"]
+let arith_module = make_dir ["Coq";"Arith";"Arith"]
+
+(* TODO: temporary hack *)
+let make_path dir id = Libnames.encode_kn dir id
+
+let nat_path = make_path datatypes_module (id_of_string "nat")
+
+let glob_nat = IndRef (nat_path,0)
+
+let path_of_O = ((nat_path,0),1)
+let path_of_S = ((nat_path,0),2)
+let glob_O = ConstructRef path_of_O
+let glob_S = ConstructRef path_of_S
+
+let eq_path = make_path logic_module (id_of_string "eq")
+let eqT_path = make_path logic_module (id_of_string "eq")
+
+let glob_eq = IndRef (eq_path,0)
+let glob_eqT = IndRef (eqT_path,0)
+
+type coq_sigma_data = {
+  proj1 : constr;
+  proj2 : constr;
+  elim  : constr;
+  intro : constr;
+  typ   : constr }
+
+type 'a delayed = unit -> 'a
+
+let build_sigma_set () =
+  { proj1 = init_constant ["Specif"] "projS1";
+    proj2 = init_constant ["Specif"] "projS2";
+    elim = init_constant ["Specif"] "sigS_rec";
+    intro = init_constant ["Specif"] "existS";
+    typ = init_constant ["Specif"] "sigS" }
+
+let build_sigma_type () =
+  { proj1 = init_constant ["Specif"] "projT1";
+    proj2 = init_constant ["Specif"] "projT2";
+    elim = init_constant ["Specif"] "sigT_rec";
+    intro = init_constant ["Specif"] "existT";
+    typ = init_constant ["Specif"] "sigT" }
+
+(* Equalities *)
+type coq_leibniz_eq_data = {
+  eq   : constr;
+  refl : constr;
+  ind  : constr;
+  rrec : constr option;
+  rect : constr option;
+  congr: constr;
+  sym  : constr }
+
+let lazy_init_constant dir id = lazy (init_constant dir id)
+
+(* Equality on Set *)
+let coq_eq_eq = lazy_init_constant ["Logic"] "eq"
+let coq_eq_refl = lazy_init_constant ["Logic"] "refl_equal"
+let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind"
+let coq_eq_rec = lazy_init_constant ["Logic"] "eq_rec"
+let coq_eq_rect = lazy_init_constant ["Logic"] "eq_rect"
+let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
+let coq_eq_sym  = lazy_init_constant ["Logic"] "sym_eq"
+let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2"
+
+let build_coq_eq_data () = {
+  eq = Lazy.force coq_eq_eq;
+  refl = Lazy.force coq_eq_refl;
+  ind = Lazy.force coq_eq_ind;
+  rrec = Some (Lazy.force coq_eq_rec);
+  rect = Some (Lazy.force coq_eq_rect);
+  congr = Lazy.force coq_eq_congr;
+  sym  = Lazy.force coq_eq_sym }
+
+let build_coq_eq () = Lazy.force coq_eq_eq
+let build_coq_f_equal2 () = Lazy.force coq_f_equal2
+
+(* Specif *)
+let coq_sumbool  = lazy_init_constant ["Specif"] "sumbool"
+
+let build_coq_sumbool () = Lazy.force coq_sumbool
+
+(* Equality on Type *)
+
+let coq_eqT_eq = lazy_init_constant ["Logic"] "eq"
+let coq_eqT_refl = lazy_init_constant ["Logic"] "refl_equal"
+let coq_eqT_ind = lazy_init_constant ["Logic"] "eq_ind"
+let coq_eqT_congr =lazy_init_constant ["Logic"] "f_equal"
+let coq_eqT_sym  = lazy_init_constant ["Logic"] "sym_eq"
+
+let build_coq_eqT_data () = {
+  eq = Lazy.force coq_eqT_eq;
+  refl = Lazy.force coq_eqT_refl;
+  ind = Lazy.force coq_eqT_ind;
+  rrec = None;
+  rect = None;
+  congr = Lazy.force coq_eqT_congr;
+  sym  = Lazy.force coq_eqT_sym }
+
+let build_coq_eqT () = Lazy.force coq_eqT_eq
+let build_coq_sym_eqT () = Lazy.force coq_eqT_sym
+
+(* Equality on Type as a Type *)
+let coq_idT_eq = lazy_init_constant ["Datatypes"] "identity"
+let coq_idT_refl = lazy_init_constant ["Datatypes"] "refl_identity"
+let coq_idT_ind = lazy_init_constant ["Datatypes"] "identity_ind"
+let coq_idT_rec = lazy_init_constant ["Datatypes"] "identity_rec"
+let coq_idT_rect = lazy_init_constant ["Datatypes"] "identity_rect"
+let coq_idT_congr = lazy_init_constant ["Logic_Type"] "congr_id"
+let coq_idT_sym = lazy_init_constant ["Logic_Type"] "sym_id"
+
+let build_coq_idT_data () = {
+  eq = Lazy.force coq_idT_eq;
+  refl = Lazy.force coq_idT_refl;
+  ind = Lazy.force coq_idT_ind;
+  rrec = Some (Lazy.force coq_idT_rec);
+  rect = Some (Lazy.force coq_idT_rect);
+  congr = Lazy.force coq_idT_congr;
+  sym  = Lazy.force coq_idT_sym }
+
+let lazy_init_constant_v7 d id id7 =
+  if !Options.v7 then lazy_init_constant d id else 
+  lazy (anomaly
+   (id7^" does no longer exist in V8 new syntax, use "^id
+    ^" instead (probably an error in ML contributed code)"))
+
+(* Empty Type *)
+let coq_EmptyT = lazy_init_constant_v7 ["Logic"] "False" "EmptyT"
+
+(* Unit Type and its unique inhabitant *)
+let coq_UnitT  = lazy_init_constant_v7 ["Datatypes"] "unit" "UnitT"
+let coq_IT     = lazy_init_constant_v7 ["Datatypes"] "tt" "IT"
+
+(* The False proposition *)
+let coq_False  = lazy_init_constant ["Logic"] "False"
+
+(* The True proposition and its unique proof *)
+let coq_True   = lazy_init_constant ["Logic"] "True"
+let coq_I      = lazy_init_constant ["Logic"] "I"
+
+(* Connectives *)
+let coq_not = lazy_init_constant ["Logic"] "not"
+let coq_and = lazy_init_constant ["Logic"] "and"
+let coq_or = lazy_init_constant ["Logic"] "or"
+let coq_ex = lazy_init_constant ["Logic"] "ex"
+
+(* Runtime part *)
+let build_coq_EmptyT () = Lazy.force coq_EmptyT
+let build_coq_UnitT () = Lazy.force coq_UnitT
+let build_coq_IT ()    = Lazy.force coq_IT
+
+let build_coq_True ()  = Lazy.force coq_True
+let build_coq_I ()     = Lazy.force coq_I
+
+let build_coq_False () = Lazy.force coq_False
+let build_coq_not ()   = Lazy.force coq_not
+let build_coq_and ()   = Lazy.force coq_and
+let build_coq_or ()   = Lazy.force coq_or
+let build_coq_ex ()   = Lazy.force coq_ex
+
+(****************************************************************************)
+(*                             Patterns                                     *)
+(* This needs to have interp_constrpattern available ... 
+
+let parse_constr s =
+  try 
+    Pcoq.parse_string Pcoq.Constr.constr_eoi s 
+  with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
+    error "Syntax error : not a construction"
+
+let parse_pattern s =
+  Constrintern.interp_constrpattern Evd.empty (Global.env()) (parse_constr s)
+let coq_eq_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Logic.eq ?1 ?2 ?3)"))
+let coq_eqT_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Logic.eq ?1 ?2 ?3)"))
+let coq_idT_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Logic_Type.identityT ?1 ?2 ?3)"))
+let coq_existS_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Specif.existS ?1 ?2 ?3 ?4)"))
+let coq_existT_pattern = 
+  lazy (snd (parse_pattern "(Coq.Init.Specif.existT ?1 ?2 ?3 ?4)"))
+let coq_not_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Logic.not ?)"))
+let coq_imp_False_pattern =
+  lazy (snd (parse_pattern "? -> Coq.Init.Logic.False"))
+let coq_imp_False_pattern =
+  lazy (snd (parse_pattern "? -> Coq.Init.Logic.False"))
+let coq_eqdec_partial_pattern =
+  lazy (snd (parse_pattern "(sumbool (eq ?1 ?2 ?3) ?4)"))
+let coq_eqdec_pattern =
+  lazy (snd (parse_pattern "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}"))
+*)
+
+(* The following is less readable but does not depend on parsing *)
+let coq_eq_ref      = lazy (init_reference ["Logic"] "eq")
+let coq_eqT_ref     = coq_eq_ref
+let coq_idT_ref     = lazy (init_reference ["Datatypes"] "identity")
+let coq_existS_ref  = lazy (init_reference ["Specif"] "existS")
+let coq_existT_ref  = lazy (init_reference ["Specif"] "existT")
+let coq_not_ref     = lazy (init_reference ["Logic"] "not")
+let coq_False_ref   = lazy (init_reference ["Logic"] "False")
+let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
+let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
new file mode 100644
index 00000000..7ac2a5c9
--- /dev/null
+++ b/interp/coqlib.mli
@@ -0,0 +1,126 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: coqlib.mli,v 1.5.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+
+(*i*)
+open Names
+open Libnames
+open Nametab
+open Term
+open Pattern
+(*i*)
+
+(*s This module collects the global references, constructions and
+    patterns of the standard library used in ocaml files *)
+
+(*s Some utilities, the first argument is used for error messages.
+    Must be used lazyly. s*)
+
+val gen_reference : string->string list -> string -> global_reference
+val gen_constant : string->string list -> string -> constr
+
+(* Search in several modules (not prefixed by "Coq") *)
+val gen_constant_in_modules : string->string list list-> string -> constr
+val arith_modules : string list list
+val zarith_base_modules : string list list
+val init_modules : string list list
+
+(*s Global references *)
+
+(* Modules *)
+val logic_module : dir_path
+val logic_type_module : dir_path
+
+(* Natural numbers *)
+val glob_nat : global_reference
+val path_of_O : constructor
+val path_of_S : constructor
+val glob_O : global_reference
+val glob_S : global_reference
+
+(* Equality *)
+val glob_eq : global_reference
+val glob_eqT : global_reference
+
+(*s Constructions and patterns related to Coq initial state are unknown
+   at compile time. Therefore, we can only provide methods to build
+   them at runtime. This is the purpose of the [constr delayed] and
+   [constr_pattern delayed] types. Objects of this time needs to be
+   applied to [()] to get the actual constr or pattern at runtime *)
+
+type 'a delayed = unit -> 'a
+
+(*s For Equality tactics *)
+type coq_sigma_data = {
+  proj1 : constr;
+  proj2 : constr;
+  elim  : constr;
+  intro : constr;
+  typ   : constr }
+
+val build_sigma_set : coq_sigma_data delayed
+val build_sigma_type : coq_sigma_data delayed
+
+type coq_leibniz_eq_data = {
+  eq   : constr;
+  refl : constr;
+  ind  : constr;
+  rrec : constr option;
+  rect : constr option;
+  congr: constr;
+  sym  : constr }
+
+val build_coq_eq_data : coq_leibniz_eq_data delayed
+val build_coq_eqT_data : coq_leibniz_eq_data delayed
+val build_coq_idT_data : coq_leibniz_eq_data delayed
+
+val build_coq_eq : constr delayed (* = (build_coq_eq_data()).eq *)
+val build_coq_f_equal2 : constr delayed
+val build_coq_eqT : constr delayed
+val build_coq_sym_eqT : constr delayed
+
+(* Empty Type *)
+val build_coq_EmptyT : constr delayed
+
+(* Unit Type and its unique inhabitant *)
+val build_coq_UnitT : constr delayed
+val build_coq_IT : constr delayed
+
+(* Specif *)
+val build_coq_sumbool : constr delayed
+
+(*s Connectives *)
+(* The False proposition *)
+val build_coq_False : constr delayed
+
+(* The True proposition and its unique proof *)
+val build_coq_True : constr delayed
+val build_coq_I : constr delayed
+
+(* Negation *)
+val build_coq_not : constr delayed
+
+(* Conjunction *)
+val build_coq_and : constr delayed
+
+(* Disjunction *)
+val build_coq_or : constr delayed
+
+(* Existential quantifier *)
+val build_coq_ex : constr delayed
+
+val coq_eq_ref : global_reference lazy_t
+val coq_eqT_ref : global_reference lazy_t
+val coq_idT_ref : global_reference lazy_t
+val coq_existS_ref : global_reference lazy_t
+val coq_existT_ref : global_reference lazy_t
+val coq_not_ref : global_reference lazy_t
+val coq_False_ref : global_reference lazy_t
+val coq_sumbool_ref : global_reference lazy_t
+val coq_sig_ref : global_reference lazy_t
diff --git a/interp/doc.tex b/interp/doc.tex
new file mode 100644
index 00000000..4d60ec34
--- /dev/null
+++ b/interp/doc.tex
@@ -0,0 +1,14 @@
+
+\newpage
+\section*{The interpretation of Coq front abstract syntax of terms}
+
+\ocwsection \label{library}
+This chapter describes the translation from \Coq\ context-dependent
+front abstract syntax of terms (\verb=front=} to and from the
+context-free, untyped, raw form of constructions (\verb=rawconstr=).
+
+The modules translating back and forth the front abstract syntax are
+organized as follows.
+
+\bigskip
+\begin{center}\epsfig{file=library.dep.ps}\end{center}
diff --git a/interp/genarg.ml b/interp/genarg.ml
new file mode 100644
index 00000000..af3d805a
--- /dev/null
+++ b/interp/genarg.ml
@@ -0,0 +1,228 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: genarg.ml,v 1.9.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Nametab
+open Rawterm
+open Topconstr
+open Term
+
+type argument_type =
+  (* Basic types *)
+  | BoolArgType
+  | IntArgType
+  | IntOrVarArgType
+  | StringArgType
+  | PreIdentArgType
+  | IntroPatternArgType
+  | IdentArgType
+  | HypArgType
+  | RefArgType
+  (* Specific types *)
+  | SortArgType
+  | ConstrArgType
+  | ConstrMayEvalArgType
+  | QuantHypArgType
+  | TacticArgType
+  | CastedOpenConstrArgType
+  | ConstrWithBindingsArgType
+  | BindingsArgType
+  | RedExprArgType
+  | List0ArgType of argument_type
+  | List1ArgType of argument_type
+  | OptArgType of argument_type
+  | PairArgType of argument_type * argument_type
+  | ExtraArgType of string
+
+type 'a or_var = ArgArg of 'a | ArgVar of identifier located
+type 'a and_short_name = 'a * identifier located option
+type rawconstr_and_expr = rawconstr * constr_expr option
+
+(* Dynamics but tagged by a type expression *)
+
+type ('a,'b) generic_argument = argument_type * Obj.t
+
+let dyntab = ref ([] : string list)
+
+type ('a,'b,'c) abstract_argument_type = argument_type
+
+let create_arg s =
+  if List.mem s !dyntab then
+    anomaly ("Genarg.create: already declared generic argument " ^ s);
+  dyntab := s :: !dyntab;
+  let t = ExtraArgType s in
+  (t,t,t)
+
+let exists_argtype s = List.mem s !dyntab
+
+type intro_pattern_expr =
+  | IntroOrAndPattern of case_intro_pattern_expr
+  | IntroWildcard
+  | IntroIdentifier of identifier
+and case_intro_pattern_expr = intro_pattern_expr list list
+
+let rec pr_intro_pattern = function
+  | IntroOrAndPattern pll -> pr_case_intro_pattern pll
+  | IntroWildcard -> str "_"
+  | IntroIdentifier id -> pr_id id
+
+and pr_case_intro_pattern = function
+  | [_::_ as pl] ->
+      str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
+  | pll ->
+      str "[" ++
+      hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
+      ++ str "]"
+
+type open_constr = Evd.evar_map * Term.constr
+type open_constr_expr = constr_expr
+type open_rawconstr = rawconstr_and_expr
+
+let rawwit_bool = BoolArgType
+let globwit_bool = BoolArgType
+let wit_bool = BoolArgType
+
+let rawwit_int = IntArgType
+let globwit_int = IntArgType
+let wit_int = IntArgType
+
+let rawwit_int_or_var = IntOrVarArgType
+let globwit_int_or_var = IntOrVarArgType
+let wit_int_or_var = IntOrVarArgType
+
+let rawwit_string = StringArgType
+let globwit_string = StringArgType
+let wit_string = StringArgType
+
+let rawwit_pre_ident = PreIdentArgType
+let globwit_pre_ident = PreIdentArgType
+let wit_pre_ident = PreIdentArgType
+
+let rawwit_intro_pattern = IntroPatternArgType
+let globwit_intro_pattern = IntroPatternArgType
+let wit_intro_pattern = IntroPatternArgType
+
+let rawwit_ident = IdentArgType
+let globwit_ident = IdentArgType
+let wit_ident = IdentArgType
+
+let rawwit_var = HypArgType
+let globwit_var = HypArgType
+let wit_var = HypArgType
+
+let rawwit_ref = RefArgType
+let globwit_ref = RefArgType
+let wit_ref = RefArgType
+
+let rawwit_quant_hyp = QuantHypArgType
+let globwit_quant_hyp = QuantHypArgType
+let wit_quant_hyp = QuantHypArgType
+
+let rawwit_sort = SortArgType
+let globwit_sort = SortArgType
+let wit_sort = SortArgType
+
+let rawwit_constr = ConstrArgType
+let globwit_constr = ConstrArgType
+let wit_constr = ConstrArgType
+
+let rawwit_constr_may_eval = ConstrMayEvalArgType
+let globwit_constr_may_eval = ConstrMayEvalArgType
+let wit_constr_may_eval = ConstrMayEvalArgType
+
+let rawwit_tactic = TacticArgType
+let globwit_tactic = TacticArgType
+let wit_tactic = TacticArgType
+
+let rawwit_casted_open_constr = CastedOpenConstrArgType
+let globwit_casted_open_constr = CastedOpenConstrArgType
+let wit_casted_open_constr = CastedOpenConstrArgType
+
+let rawwit_constr_with_bindings = ConstrWithBindingsArgType
+let globwit_constr_with_bindings = ConstrWithBindingsArgType
+let wit_constr_with_bindings = ConstrWithBindingsArgType
+
+let rawwit_bindings = BindingsArgType
+let globwit_bindings = BindingsArgType
+let wit_bindings = BindingsArgType
+
+let rawwit_red_expr = RedExprArgType
+let globwit_red_expr = RedExprArgType
+let wit_red_expr = RedExprArgType
+
+let wit_list0 t = List0ArgType t
+
+let wit_list1 t = List1ArgType t
+
+let wit_opt t = OptArgType t
+
+let wit_pair t1 t2 = PairArgType (t1,t2)
+
+let in_gen t o = (t,Obj.repr o)
+let out_gen t (t',o) = if t = t' then Obj.magic o else failwith "out_gen"
+let genarg_tag (s,_) = s
+
+let fold_list0 f = function
+  | (List0ArgType t as u, l) ->
+      List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l)
+  | _ -> failwith "Genarg: not a list0"
+
+let fold_list1 f = function
+  | (List1ArgType t as u, l) ->
+      List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l)
+  | _ -> failwith "Genarg: not a list1"
+
+let fold_opt f a = function
+  | (OptArgType t as u, l) ->
+      (match Obj.magic l with
+	| None -> a
+	| Some x -> f (in_gen t x))
+  | _ -> failwith "Genarg: not a opt"
+
+let fold_pair f = function
+  | (PairArgType (t1,t2) as u, l) ->
+      let (x1,x2) = Obj.magic l in
+      f (in_gen t1 x1) (in_gen t2 x2)
+  | _ -> failwith "Genarg: not a pair"
+
+let app_list0 f = function
+  | (List0ArgType t as u, l) ->
+      let o = Obj.magic l in
+      (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o))
+  | _ -> failwith "Genarg: not a list0"
+
+let app_list1 f = function
+  | (List1ArgType t as u, l) ->
+      let o = Obj.magic l in
+      (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o))
+  | _ -> failwith "Genarg: not a list1"
+
+let app_opt f = function
+  | (OptArgType t as u, l) ->
+      let o = Obj.magic l in
+      (u, Obj.repr (option_app (fun x -> out_gen t (f (in_gen t x))) o))
+  | _ -> failwith "Genarg: not an opt"
+
+let app_pair f1 f2 = function
+  | (PairArgType (t1,t2) as u, l) ->
+      let (o1,o2) = Obj.magic l in
+      let o1 = out_gen t1 (f1 (in_gen t1 o1)) in
+      let o2 = out_gen t2 (f2 (in_gen t2 o2)) in
+      (u, Obj.repr (o1,o2))
+  | _ -> failwith "Genarg: not a pair"
+
+let unquote x = x
+
+type an_arg_of_this_type = Obj.t
+
+let in_generic t x = (t, Obj.repr x)
diff --git a/interp/genarg.mli b/interp/genarg.mli
new file mode 100644
index 00000000..59b6e10d
--- /dev/null
+++ b/interp/genarg.mli
@@ -0,0 +1,262 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: genarg.mli,v 1.9.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+
+open Util
+open Names
+open Term
+open Libnames
+open Rawterm
+open Topconstr
+open Term
+
+type 'a or_var = ArgArg of 'a | ArgVar of identifier located
+type 'a and_short_name = 'a * identifier located option
+
+(* In globalize tactics, we need to keep the initial constr_expr to recompute*)
+(* in the environment by the effective calls to Intro, Inversion, etc *)
+(* The constr_expr field is None in TacDef though *)
+type rawconstr_and_expr = rawconstr * constr_expr option
+
+type open_constr = Evd.evar_map * Term.constr
+type open_constr_expr = constr_expr
+type open_rawconstr = rawconstr_and_expr
+
+type intro_pattern_expr =
+  | IntroOrAndPattern of case_intro_pattern_expr
+  | IntroWildcard
+  | IntroIdentifier of identifier
+and case_intro_pattern_expr = intro_pattern_expr list list
+
+val pr_intro_pattern : intro_pattern_expr -> Pp.std_ppcmds
+val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds
+
+(* The route of a generic argument, from parsing to evaluation
+
+              parsing        in_raw                           out_raw
+    char stream ----> rawtype ----> rawconstr generic_argument ---->
+                                                                   |
+                                                                   | interp
+                                                                   V
+                          type  <---- constr generic_argument  <----
+                                  out                            in
+
+To distinguish between the uninterpreted (raw) and the interpreted
+worlds, we annotate the type generic_argument by a phantom argument
+which is either constr_expr or constr (actually we add also a second
+argument raw_tactic_expr and tactic, but this is only for technical
+reasons, because these types are undefined at the type of compilation
+of Genarg).
+
+Transformation for each type :
+tag   f                          raw open type          cooked closed type
+
+BoolArgType                    bool                     bool
+IntArgType                     int                      int
+IntOrVarArgType                int or_var               int
+StringArgType                  string (parsed w/ "")    string
+PreIdentArgType                string (parsed w/o "")   (vernac only)
+IdentArgType                   identifier               identifier
+IntroPatternArgType            intro_pattern_expr       intro_pattern_expr
+VarArgType                     identifier               constr
+RefArgType                     reference                global_reference
+ConstrArgType                  constr_expr              constr
+ConstrMayEvalArgType           constr_expr may_eval     constr
+QuantHypArgType                quantified_hypothesis    quantified_hypothesis
+TacticArgType                  raw_tactic_expr          tactic
+CastedOpenConstrArgType        constr_expr              open_constr
+ConstrBindingsArgType      constr_expr with_bindings constr with_bindings
+List0ArgType of argument_type
+List1ArgType of argument_type
+OptArgType of argument_type
+ExtraArgType of string         '_a                      '_b
+*)
+
+type ('a,'co,'ta) abstract_argument_type
+
+val rawwit_bool : (bool,'co,'ta) abstract_argument_type
+val globwit_bool : (bool,'co,'ta) abstract_argument_type
+val wit_bool : (bool,'co,'ta) abstract_argument_type
+
+val rawwit_int : (int,'co,'ta) abstract_argument_type
+val globwit_int : (int,'co,'ta) abstract_argument_type
+val wit_int : (int,'co,'ta) abstract_argument_type
+
+val rawwit_int_or_var : (int or_var,'co,'ta) abstract_argument_type
+val globwit_int_or_var : (int or_var,'co,'ta) abstract_argument_type
+val wit_int_or_var : (int or_var,'co,'ta) abstract_argument_type
+
+val rawwit_string : (string,'co,'ta) abstract_argument_type
+val globwit_string : (string,'co,'ta) abstract_argument_type
+val wit_string : (string,'co,'ta) abstract_argument_type
+
+val rawwit_pre_ident : (string,'co,'ta) abstract_argument_type
+val globwit_pre_ident : (string,'co,'ta) abstract_argument_type
+val wit_pre_ident : (string,'co,'ta) abstract_argument_type
+
+val rawwit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
+val globwit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
+val wit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
+
+val rawwit_ident : (identifier,'co,'ta) abstract_argument_type
+val globwit_ident : (identifier,'co,'ta) abstract_argument_type
+val wit_ident : (identifier,'co,'ta) abstract_argument_type
+
+val rawwit_var : (identifier located,'co,'ta) abstract_argument_type
+val globwit_var : (identifier located,'co,'ta) abstract_argument_type
+val wit_var : ('co,'co,'ta) abstract_argument_type
+
+val rawwit_ref : (reference,constr_expr,'ta) abstract_argument_type
+val globwit_ref : (global_reference located or_var,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_ref : (global_reference,constr,'ta) abstract_argument_type
+
+val rawwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type
+val globwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type
+val wit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type
+
+val rawwit_sort : (rawsort,constr_expr,'ta) abstract_argument_type
+val globwit_sort : (rawsort,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_sort : (sorts,constr,'ta) abstract_argument_type
+
+val rawwit_constr : (constr_expr,constr_expr,'ta) abstract_argument_type
+val globwit_constr : (rawconstr_and_expr,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_constr : (constr,constr,'ta) abstract_argument_type
+
+val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,constr_expr,'ta) abstract_argument_type
+val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type
+
+val rawwit_casted_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type
+val globwit_casted_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_casted_open_constr : (open_constr,constr,'ta) abstract_argument_type
+
+val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) abstract_argument_type
+val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type
+
+val rawwit_bindings : (constr_expr bindings,constr_expr,'ta) abstract_argument_type
+val globwit_bindings : (rawconstr_and_expr bindings,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_bindings : (constr bindings,constr,'ta) abstract_argument_type
+
+val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,constr_expr,'ta) abstract_argument_type
+val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,constr,'ta) abstract_argument_type
+
+(* TODO: transformer tactic en extra arg *)
+val rawwit_tactic : ('ta,constr_expr,'ta) abstract_argument_type
+val globwit_tactic : ('ta,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_tactic : ('ta,constr,'ta) abstract_argument_type
+
+val wit_list0 :
+  ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
+
+val wit_list1 :
+  ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
+
+val wit_opt :
+  ('a,'co,'ta) abstract_argument_type -> ('a option,'co,'ta) abstract_argument_type
+
+val wit_pair :
+  ('a,'co,'ta) abstract_argument_type ->
+  ('b,'co,'ta) abstract_argument_type ->
+      ('a * 'b,'co,'ta) abstract_argument_type
+
+(* 'a generic_argument = (Sigma t:type. t[constr/'a]) *)
+type ('a,'b) generic_argument
+
+val fold_list0 : 
+ (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c
+
+val fold_list1 : 
+ (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c
+
+val fold_opt :
+ (('a,'b) generic_argument -> 'c) -> 'c -> ('a,'b) generic_argument -> 'c
+
+val fold_pair :
+ (('a,'b) generic_argument -> ('a,'b) generic_argument -> 'c) -> 
+      ('a,'b) generic_argument -> 'c
+
+(* [app_list0] fails if applied to an argument not of tag [List0 t]
+    for some [t]; it's the responsability of the caller to ensure it *)
+
+val app_list0 : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> 
+('a,'b) generic_argument -> ('c,'d) generic_argument
+
+val app_list1 : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> 
+('a,'b) generic_argument -> ('c,'d) generic_argument
+
+val app_opt : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> 
+('a,'b) generic_argument -> ('c,'d) generic_argument
+
+val app_pair :
+  (('a,'b) generic_argument -> ('c,'d) generic_argument) ->
+      (('a,'b) generic_argument -> ('c,'d) generic_argument)
+   -> ('a,'b) generic_argument -> ('c,'d) generic_argument
+
+(* Manque l'ordre supérieur, on aimerait ('co,'ta) 'a; manque aussi le
+   polymorphism, on aimerait que 'b et 'c restent polymorphes à l'appel
+   de create *)
+val create_arg : string ->
+      ('a,'co,'ta) abstract_argument_type
+      * ('globa,'globco,'globta) abstract_argument_type
+      * ('rawa,'rawco,'rawta) abstract_argument_type
+
+val exists_argtype : string -> bool
+
+type argument_type =
+  (* Basic types *)
+  | BoolArgType
+  | IntArgType
+  | IntOrVarArgType
+  | StringArgType
+  | PreIdentArgType
+  | IntroPatternArgType
+  | IdentArgType
+  | HypArgType
+  | RefArgType
+  (* Specific types *)
+  | SortArgType
+  | ConstrArgType
+  | ConstrMayEvalArgType
+  | QuantHypArgType
+  | TacticArgType
+  | CastedOpenConstrArgType
+  | ConstrWithBindingsArgType
+  | BindingsArgType
+  | RedExprArgType
+  | List0ArgType of argument_type
+  | List1ArgType of argument_type
+  | OptArgType of argument_type
+  | PairArgType of argument_type * argument_type
+  | ExtraArgType of string
+
+val genarg_tag : ('a,'b) generic_argument -> argument_type
+
+val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type
+
+(* We'd like
+
+  [in_generic: !b:type, !a:argument_type -> (f a) -> b generic_argument]
+
+   with f a = b if a is Constr, f a = c if a is Tactic, otherwise f a = |a|
+
+   in_generic is not typable; we replace the second argument by an absurd
+   type (with no introduction rule)
+*)
+type an_arg_of_this_type
+
+val in_generic : 
+  argument_type -> an_arg_of_this_type -> ('a,'b) generic_argument
+
+val in_gen :
+  ('a,'co,'ta) abstract_argument_type -> 'a -> ('co,'ta) generic_argument
+val out_gen :
+  ('a,'co,'ta) abstract_argument_type -> ('co,'ta) generic_argument -> 'a 
+
diff --git a/interp/modintern.ml b/interp/modintern.ml
new file mode 100644
index 00000000..0929119c
--- /dev/null
+++ b/interp/modintern.ml
@@ -0,0 +1,103 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: modintern.ml,v 1.2.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Entries
+open Libnames
+open Topconstr
+open Constrintern
+ 
+let rec make_mp mp = function
+    [] -> mp
+  | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
+
+(*
+(* Since module components are not put in the nametab we try to locate
+the module prefix *)
+exception BadRef
+
+let lookup_qualid (modtype:bool) qid = 
+  let rec make_mp mp = function
+      [] -> mp
+    | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
+  in
+  let rec find_module_prefix dir n =
+    if n<0 then raise Not_found;
+    let dir',dir'' = list_chop n dir in
+    let id',dir''' = 
+      match dir'' with 
+	| hd::tl -> hd,tl 
+	| _ -> anomaly "This list should not be empty!"
+    in
+    let qid' = make_qualid dir' id' in
+      try 
+	match Nametab.locate qid' with
+	  | ModRef mp -> mp,dir'''
+	  | _ -> raise BadRef
+      with
+	  Not_found -> find_module_prefix dir (pred n)
+  in
+    try Nametab.locate qid
+    with Not_found -> 
+      let (dir,id) = repr_qualid qid in
+      let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in
+      let mp = 
+	List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir' 
+      in
+	if modtype then
+	  ModTypeRef (make_ln mp (label_of_id id))
+	else
+	  ModRef (MPdot (mp,label_of_id id))
+
+*)
+
+(* Search for the head of [qid] in [binders]. 
+   If found, returns the module_path/kernel_name created from the dirpath
+   and the basename. Searches Nametab otherwise.
+*)
+
+let lookup_module (loc,qid) =
+  try
+    Nametab.locate_module qid
+  with
+    | Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid)
+	
+let lookup_modtype (loc,qid) =
+  try
+    Nametab.locate_modtype qid
+  with
+    | Not_found -> 
+	Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
+
+let transl_with_decl env = function 
+  | CWith_Module ((_,id),qid) ->
+      With_Module (id,lookup_module qid)
+  | CWith_Definition ((_,id),c) ->
+      With_Definition (id,interp_constr Evd.empty env c)
+
+let rec interp_modtype env = function 
+  | CMTEident qid ->
+      MTEident (lookup_modtype qid)
+  | CMTEwith (mty,decl) ->
+      let mty = interp_modtype env mty in
+      let decl = transl_with_decl env decl in
+	MTEwith(mty,decl)
+ 
+
+let rec interp_modexpr env = function 
+  | CMEident qid ->
+      MEident (lookup_module qid)
+  | CMEapply (me1,me2) ->
+      let me1 = interp_modexpr env me1 in
+      let me2 = interp_modexpr env me2 in
+	MEapply(me1,me2)
+
diff --git a/interp/modintern.mli b/interp/modintern.mli
new file mode 100644
index 00000000..050d9f94
--- /dev/null
+++ b/interp/modintern.mli
@@ -0,0 +1,24 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: modintern.mli,v 1.1.6.1 2004/07/16 19:30:22 herbelin Exp $ i*)
+
+(*i*)
+open Declarations
+open Environ
+open Entries
+open Topconstr
+(*i*)
+
+(* Module expressions and module types are interpreted relatively to 
+   eventual functor or funsig arguments. *)
+
+val interp_modtype : env -> module_type_ast -> module_type_entry
+
+val interp_modexpr : env -> module_ast -> module_expr
+
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
new file mode 100644
index 00000000..29fb7cc7
--- /dev/null
+++ b/interp/ppextend.ml
@@ -0,0 +1,58 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: ppextend.ml,v 1.4.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+
+(*i*)
+open Pp
+open Util
+open Names
+(*i*)
+
+(*s Pretty-print. *)
+
+(* Dealing with precedences *)
+
+type precedence = int
+
+type parenRelation = L | E | Any | Prec of precedence
+
+type tolerability = precedence * parenRelation
+
+type ppbox =
+  | PpHB of int
+  | PpHOVB of int
+  | PpHVB of int
+  | PpVB of int
+  | PpTB
+
+type ppcut =
+  | PpBrk of int * int
+  | PpTbrk of int * int
+  | PpTab
+  | PpFnl
+
+let ppcmd_of_box = function
+  | PpHB n -> h n
+  | PpHOVB n -> hov n
+  | PpHVB n -> hv n
+  | PpVB n -> v n
+  | PpTB   -> t
+
+let ppcmd_of_cut = function
+  | PpTab -> tab ()
+  | PpFnl -> fnl ()
+  | PpBrk(n1,n2) -> brk(n1,n2)
+  | PpTbrk(n1,n2) -> tbrk(n1,n2)
+
+type unparsing = 
+  | UnpMetaVar of int * parenRelation
+  | UnpListMetaVar of int * parenRelation * unparsing list
+  | UnpTerminal of string
+  | UnpBox of ppbox * unparsing list
+  | UnpCut of ppcut
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
new file mode 100644
index 00000000..056b7a42
--- /dev/null
+++ b/interp/ppextend.mli
@@ -0,0 +1,48 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: ppextend.mli,v 1.4.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+
+(*i*)
+open Pp
+open Names
+(*i*)
+
+(*s Pretty-print. *)
+
+(* Dealing with precedences *)
+
+type precedence = int
+
+type parenRelation = L | E | Any | Prec of precedence
+
+type tolerability = precedence * parenRelation
+
+type ppbox =
+  | PpHB of int
+  | PpHOVB of int
+  | PpHVB of int
+  | PpVB of int
+  | PpTB
+
+type ppcut =
+  | PpBrk of int * int
+  | PpTbrk of int * int
+  | PpTab
+  | PpFnl
+
+val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
+
+val ppcmd_of_cut : ppcut -> std_ppcmds
+
+type unparsing = 
+  | UnpMetaVar of int * parenRelation
+  | UnpListMetaVar of int * parenRelation * unparsing list
+  | UnpTerminal of string
+  | UnpBox of ppbox * unparsing list
+  | UnpCut of ppcut
diff --git a/interp/reserve.ml b/interp/reserve.ml
new file mode 100644
index 00000000..72899676
--- /dev/null
+++ b/interp/reserve.ml
@@ -0,0 +1,95 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: reserve.ml,v 1.10.2.1 2004/07/16 19:30:22 herbelin Exp $ i*)
+
+(* Reserved names *)
+
+open Util
+open Pp
+open Names
+open Nameops
+open Summary
+open Libobject
+open Lib
+
+let reserve_table = ref Idmap.empty
+
+let cache_reserved_type (_,(id,t)) =
+  reserve_table := Idmap.add id t !reserve_table
+
+let (in_reserved, _) =
+  declare_object {(default_object "RESERVED-TYPE") with 
+    cache_function = cache_reserved_type }
+
+let _ = 
+  Summary.declare_summary "reserved-type"
+    { Summary.freeze_function = (fun () -> !reserve_table);
+      Summary.unfreeze_function = (fun r -> reserve_table := r);
+      Summary.init_function = (fun () -> reserve_table := Idmap.empty);
+      Summary.survive_module = false;
+      Summary.survive_section = false }
+
+let declare_reserved_type (loc,id) t = 
+  if id <> root_of_id id then
+    user_err_loc(loc,"declare_reserved_type",
+    (pr_id id ++ str
+      " is not reservable: it must have no trailing digits, quote, or _"));
+  begin try
+    let _ = Idmap.find id !reserve_table in 
+    user_err_loc(loc,"declare_reserved_type",
+    (pr_id id++str" is already bound to a type"))
+  with Not_found -> () end;
+  add_anonymous_leaf (in_reserved (id,t))
+
+let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table
+
+open Rawterm
+
+let rec unloc = function
+  | RVar (_,id) -> RVar (dummy_loc,id)
+  | RApp (_,g,args) -> RApp (dummy_loc,unloc g, List.map unloc args)
+  | RLambda (_,na,ty,c) -> RLambda (dummy_loc,na,unloc ty,unloc c)
+  | RProd (_,na,ty,c) -> RProd (dummy_loc,na,unloc ty,unloc c)
+  | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
+  | RCases (_,(tyopt,rtntypopt),tml,pl) ->
+      RCases (dummy_loc,
+        (option_app unloc tyopt,ref (option_app unloc !rtntypopt)),
+	List.map (fun (tm,x) -> (unloc tm,x)) tml,
+        List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
+  | ROrderedCase (_,b,tyopt,tm,bv,x) ->
+      ROrderedCase 
+      (dummy_loc,b,option_app unloc tyopt,unloc tm, Array.map unloc bv,x)
+  | RLetTuple (_,nal,(na,po),b,c) ->
+      RLetTuple (dummy_loc,nal,(na,option_app unloc po),unloc b,unloc c)
+  | RIf (_,c,(na,po),b1,b2) ->
+      RIf (dummy_loc,unloc c,(na,option_app unloc po),unloc b1,unloc b2)
+  | RRec (_,fk,idl,bl,tyl,bv) ->
+      RRec (dummy_loc,fk,idl,
+            Array.map (List.map 
+              (fun (na,obd,ty) -> (na,option_app unloc obd, unloc ty)))
+              bl,
+            Array.map unloc tyl,
+            Array.map unloc bv)
+  | RCast (_,c,t) -> RCast (dummy_loc,unloc c,unloc t)
+  | RSort (_,x) -> RSort (dummy_loc,x)
+  | RHole (_,x)  -> RHole (dummy_loc,x)
+  | RRef (_,x) -> RRef (dummy_loc,x)
+  | REvar (_,x,l) -> REvar (dummy_loc,x,l)
+  | RPatVar (_,x) -> RPatVar (dummy_loc,x)
+  | RDynamic (_,x) -> RDynamic (dummy_loc,x)
+
+let anonymize_if_reserved na t = match na with
+  | Name id as na ->
+      if !Options.v7 & id = id_of_string "_" then t else
+      (try 
+	if unloc t = find_reserved_type id
+	then RHole (dummy_loc,BinderType na)
+	else t
+      with Not_found -> t)
+  | Anonymous -> t
diff --git a/interp/reserve.mli b/interp/reserve.mli
new file mode 100644
index 00000000..a79e2c25
--- /dev/null
+++ b/interp/reserve.mli
@@ -0,0 +1,17 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: reserve.mli,v 1.2.2.1 2004/07/16 19:30:22 herbelin Exp $ i*)
+
+open Util
+open Names
+open Rawterm
+
+val declare_reserved_type : identifier located -> rawconstr -> unit
+val find_reserved_type : identifier -> rawconstr
+val anonymize_if_reserved : name -> rawconstr -> rawconstr
diff --git a/interp/symbols.ml b/interp/symbols.ml
new file mode 100644
index 00000000..ed151d8e
--- /dev/null
+++ b/interp/symbols.ml
@@ -0,0 +1,662 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: symbols.ml,v 1.31.2.1 2004/07/16 19:30:23 herbelin Exp $ *)
+
+(*i*)
+open Util
+open Pp
+open Bignat
+open Names
+open Nametab
+open Libnames
+open Summary
+open Rawterm
+open Topconstr
+open Ppextend
+(*i*)
+
+(*s A scope is a set of notations; it includes
+
+  - a set of ML interpreters/parsers for positive (e.g. 0, 1, 15, ...) and
+    negative numbers (e.g. -0, -2, -13, ...). These interpreters may
+    fail if a number has no interpretation in the scope (e.g. there is
+    no interpretation for negative numbers in [nat]); interpreters both for
+    terms and patterns can be set; these interpreters are in permanent table
+    [numeral_interpreter_tab]
+  - a set of ML printers for expressions denoting numbers parsable in 
+    this scope (permanently declared in [Esyntax.primitive_printer_tab])
+  - a set of interpretations for infix (more generally distfix) notations
+  - an optional pair of delimiters which, when occurring in a syntactic
+    expression, set this scope to be the current scope
+*)
+
+(**********************************************************************)
+(* Scope of symbols *)
+
+type level = precedence * tolerability list
+type delimiters = string
+
+type scope = {
+  notations: (interpretation * (dir_path * string) * bool) Stringmap.t;
+  delimiters: delimiters option
+}
+
+(* Uninterpreted notation map: notation -> level * dir_path *)
+let notation_level_map = ref Stringmap.empty
+
+(* Scopes table: scope_name -> symbol_interpretation *)
+let scope_map = ref Stringmap.empty
+
+let empty_scope = {
+  notations = Stringmap.empty;
+  delimiters = None
+}
+
+let default_scope = "" (* empty name, not available from outside *)
+let type_scope = "type_scope" (* special scope used for interpreting types *)
+
+let init_scope_map () =
+  scope_map := Stringmap.add default_scope empty_scope !scope_map;
+  scope_map := Stringmap.add type_scope empty_scope !scope_map
+
+(**********************************************************************)
+(* Operations on scopes *)
+
+let declare_scope scope =
+  try let _ = Stringmap.find scope !scope_map in ()
+  with Not_found ->
+(*    Options.if_verbose message ("Creating scope "^scope);*)
+    scope_map := Stringmap.add scope empty_scope !scope_map
+
+let find_scope scope =
+  try Stringmap.find scope !scope_map
+  with Not_found -> error ("Scope "^scope^" is not declared")
+
+let check_scope sc = let _ = find_scope sc in ()
+
+(**********************************************************************)
+(* The global stack of scopes                                         *)
+
+type scope_elem = Scope of scope_name | SingleNotation of string
+type scopes = scope_elem list
+
+let scope_stack = ref []
+
+let current_scopes () = !scope_stack
+
+(* TODO: push nat_scope, z_scope, ... in scopes summary *)
+
+(* Exportation of scopes *)
+let cache_scope (_,(local,op,sc)) =
+  (match sc with Scope sc -> check_scope sc | _ -> ());
+  scope_stack := if op then sc :: !scope_stack else list_except sc !scope_stack
+
+let subst_scope (_,subst,sc) = sc
+
+open Libobject
+
+let classify_scope (_,(local,_,_ as o)) =
+  if local then Dispose else Substitute o
+
+let export_scope (local,_,_ as x) = if local then None else Some x
+
+let (inScope,outScope) = 
+  declare_object {(default_object "SCOPE") with
+      cache_function = cache_scope;
+      open_function = (fun i o -> if i=1 then cache_scope o);
+      subst_function = subst_scope;
+      classify_function = classify_scope;
+      export_function = export_scope }
+
+let open_close_scope (local,opening,sc) =
+  Lib.add_anonymous_leaf (inScope (local,opening,Scope sc))
+
+let empty_scope_stack = []
+
+let push_scope sc scopes = Scope sc :: scopes
+
+(**********************************************************************)
+(* Delimiters *)
+
+let delimiters_map = ref Stringmap.empty
+
+let declare_delimiters scope key =
+  let sc = find_scope scope in
+  if sc.delimiters <> None && Options.is_verbose () then begin
+    let old = out_some sc.delimiters in
+    Options.if_verbose 
+      warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
+  end;
+  let sc = { sc with delimiters = Some key } in
+  scope_map := Stringmap.add scope sc !scope_map;
+  if Stringmap.mem key !delimiters_map then begin
+    let oldsc = Stringmap.find key !delimiters_map in
+    Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
+  end;
+  delimiters_map := Stringmap.add key scope !delimiters_map
+
+let find_delimiters_scope loc key = 
+  try Stringmap.find key !delimiters_map
+  with Not_found -> 
+    user_err_loc 
+    (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
+
+(* Uninterpretation tables *)
+
+type interp_rule =
+  | NotationRule of scope_name option * notation
+  | SynDefRule of kernel_name
+
+(* We define keys for rawterm and aconstr to split the syntax entries
+   according to the key of the pattern (adapted from Chet Murthy by HH) *)
+
+type key =
+  | RefKey of global_reference
+  | Oth
+
+(* Scopes table : interpretation -> scope_name *)
+let notations_key_table = ref Gmapl.empty
+let numeral_key_table = Hashtbl.create 7
+
+let rawconstr_key = function
+  | RApp (_,RRef (_,ref),_) -> RefKey ref
+  | RRef (_,ref) -> RefKey ref
+  | _ -> Oth
+
+let cases_pattern_key = function
+  | PatCstr (_,ref,_,_) -> RefKey (ConstructRef ref)
+  | _ -> Oth
+
+let aconstr_key = function
+  | AApp (ARef ref,args) -> RefKey ref, Some (List.length args)
+  | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey ref, Some (List.length args)
+  | ARef ref -> RefKey ref, Some 0
+  | _ -> Oth, None
+
+let pattern_key = function
+  | PatCstr (_,cstr,_,_) -> RefKey (ConstructRef cstr)
+  | _ -> Oth
+
+(**********************************************************************)
+(* Interpreting numbers (not in summary because functional objects)   *)
+
+type num_interpreter =
+    (loc -> bigint -> rawconstr)
+    * (loc -> bigint -> name -> cases_pattern) option
+
+type num_uninterpreter =
+    rawconstr list * (rawconstr -> bigint option)
+    * (cases_pattern -> bigint option) option
+
+type required_module = global_reference * string list 
+
+let numeral_interpreter_tab =
+  (Hashtbl.create 7 : (scope_name,required_module*num_interpreter) Hashtbl.t)
+
+let declare_numeral_interpreter sc dir interp (patl,uninterp,uninterpc) =
+  declare_scope sc;
+  Hashtbl.add numeral_interpreter_tab sc (dir,interp);
+  List.iter
+    (fun pat -> Hashtbl.add numeral_key_table (rawconstr_key pat)
+      (sc,uninterp,uninterpc))
+    patl
+
+let check_required_module loc sc (ref,d) =
+  let d' = List.map id_of_string d in
+  let dir = make_dirpath (List.rev d') in
+  try let _ = sp_of_global ref in ()
+  with Not_found ->
+    user_err_loc (loc,"numeral_interpreter",
+    str ("Cannot interpret numbers in "^sc^" without requiring first module "
+    ^(list_last d)))
+
+let lookup_numeral_interpreter loc = function
+  | Scope sc ->
+      let (dir,interpreter) = Hashtbl.find numeral_interpreter_tab sc in
+      check_required_module loc sc dir;
+      interpreter
+  | SingleNotation _ -> raise Not_found
+
+(* Look if some notation or numeral printer in [scope] can be used in
+   the scope stack [scopes], and if yes, using delimiters or not *)
+
+let find_with_delimiters = function
+  | None -> None
+  | Some scope ->
+      match (Stringmap.find scope !scope_map).delimiters with
+	| Some key -> Some (Some scope, Some key)
+	| None -> None
+
+let rec find_without_delimiters find (ntn_scope,ntn) = function
+  | Scope scope :: scopes -> 
+      (* Is the expected ntn/numpr attached to the most recently open scope? *)
+      if Some scope = ntn_scope then
+	Some (None,None)
+      else
+	(* If the most recently open scope has a notation/numeral printer
+    	   but not the expected one then we need delimiters *)
+	if find scope then
+	  find_with_delimiters ntn_scope
+	else
+	  find_without_delimiters find (ntn_scope,ntn) scopes
+  | SingleNotation ntn' :: scopes ->
+      if ntn_scope = None & ntn = Some ntn' then 
+	Some (None,None)
+      else
+	find_without_delimiters find (ntn_scope,ntn) scopes
+  | [] ->
+      (* Can we switch to [scope]? Yes if it has defined delimiters *)
+      find_with_delimiters ntn_scope
+
+(* Uninterpreted notation levels *)
+
+let declare_notation_level ntn level =
+  if not !Options.v7 & Stringmap.mem ntn !notation_level_map then
+    error ("Notation "^ntn^" is already assigned a level");
+  notation_level_map := Stringmap.add ntn level !notation_level_map
+
+let level_of_notation ntn =
+  Stringmap.find ntn !notation_level_map
+
+(* The mapping between notations and their interpretation *)
+
+let declare_notation_interpretation ntn scopt pat df pp8only =
+  let scope = match scopt with Some s -> s | None -> default_scope in
+  let sc = find_scope scope in
+  if Stringmap.mem ntn sc.notations && Options.is_verbose () then
+    warning ("Notation "^ntn^" is already used"^
+    (if scopt = None then "" else " in scope "^scope));
+  let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in
+  scope_map := Stringmap.add scope sc !scope_map;
+  if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
+
+let declare_uninterpretation rule (metas,c as pat) =
+  let (key,n) = aconstr_key c in
+  notations_key_table := Gmapl.add key (rule,pat,n) !notations_key_table
+
+let rec find_interpretation f = function
+  | sce :: scopes ->
+      let scope = match sce with
+	| Scope s -> s 
+	| SingleNotation _ -> default_scope in
+      (try f scope
+      with Not_found -> find_interpretation f scopes)
+  | [] -> raise Not_found
+
+let rec interp_notation loc ntn scopes =
+  let f sc =
+    let scope = find_scope sc in
+    let (pat,df,pp8only) = Stringmap.find ntn scope.notations in
+    if pp8only then raise Not_found;
+    pat,(df,if sc = default_scope then None else Some sc) in
+  try find_interpretation f (List.fold_right push_scope scopes !scope_stack)
+  with Not_found -> 
+    user_err_loc
+      (loc,"",str ("Unknown interpretation for notation \""^ntn^"\""))
+
+let uninterp_notations c =
+  Gmapl.find (rawconstr_key c) !notations_key_table
+
+let uninterp_cases_pattern_notations c =
+  Gmapl.find (cases_pattern_key c) !notations_key_table
+
+let availability_of_notation (ntn_scope,ntn) scopes =
+  let f scope =
+    Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
+  find_without_delimiters f (ntn_scope,Some ntn) scopes
+
+let rec interp_numeral_gen loc f n = function
+  | scope :: scopes ->
+      (try f (lookup_numeral_interpreter loc scope)
+       with Not_found -> interp_numeral_gen loc f n scopes)
+  | [] ->
+      user_err_loc (loc,"interp_numeral",
+      str "No interpretation for numeral " ++ pr_bigint n)
+
+let interp_numeral loc n scopes =
+  interp_numeral_gen loc (fun x -> fst x loc n) n
+    (List.fold_right push_scope scopes !scope_stack)
+
+let interp_numeral_as_pattern loc n name scopes =
+  let f x = match snd x with
+    | None -> raise Not_found
+    | Some g -> g loc n name in
+  interp_numeral_gen loc f n (List.fold_right push_scope scopes !scope_stack)
+
+let uninterp_numeral c =
+  try 
+    let (sc,numpr,_) = Hashtbl.find numeral_key_table (rawconstr_key c) in
+    match numpr c with
+      | None -> raise No_match
+      | Some n -> (sc,n)
+  with Not_found -> raise No_match
+
+let uninterp_cases_numeral c =
+  try 
+    match Hashtbl.find numeral_key_table (pattern_key c) with
+      | (_,_,None) -> raise No_match
+      | (sc,_,Some numpr) ->
+	  match numpr c with
+	    | None -> raise No_match
+	    | Some n -> (sc,n)
+  with Not_found -> raise No_match
+
+let availability_of_numeral printer_scope scopes =
+  let f scope = Hashtbl.mem numeral_interpreter_tab scope in
+  option_app snd (find_without_delimiters f (Some printer_scope,None) scopes)
+
+(* Miscellaneous *)
+
+let exists_notation_in_scope scopt ntn r =
+  let scope = match scopt with Some s -> s | None -> default_scope in
+  try
+    let sc = Stringmap.find scope !scope_map in
+    let (r',_,pp8only) = Stringmap.find ntn sc.notations in
+    r' = r, pp8only
+  with Not_found -> false, false
+
+(* Special scopes associated to arguments of a global reference *)
+
+let arguments_scope = ref Refmap.empty
+
+let cache_arguments_scope (_,(r,scl)) =
+  List.iter (option_iter check_scope) scl;
+  arguments_scope := Refmap.add r scl !arguments_scope
+
+let subst_arguments_scope (_,subst,(r,scl)) = (subst_global subst r,scl)
+
+let (inArgumentsScope,outArgumentsScope) = 
+  declare_object {(default_object "ARGUMENTS-SCOPE") with
+      cache_function = cache_arguments_scope;
+      load_function = (fun _ o -> cache_arguments_scope o);
+      subst_function = subst_arguments_scope;
+      classify_function = (fun (_,o) -> Substitute o);
+      export_function = (fun x -> Some x) }
+
+let declare_arguments_scope r scl =
+  Lib.add_anonymous_leaf (inArgumentsScope (r,scl))
+
+let find_arguments_scope r =
+  try Refmap.find r !arguments_scope
+  with Not_found -> []
+
+(**********************************************************************)
+(* Mapping classes to scopes *)
+
+open Classops
+
+let class_scope_map = ref (Gmap.empty : (cl_typ,scope_name) Gmap.t)
+
+let _ = Gmap.add CL_SORT "type_scope" Gmap.empty
+
+let declare_class_scope sc cl =
+  class_scope_map := Gmap.add cl sc !class_scope_map
+
+let find_class_scope cl =
+  Gmap.find cl !class_scope_map
+
+open Term
+
+let find_class t =
+  let t, _ = decompose_app (Reductionops.whd_betaiotazeta t) in
+  match kind_of_term t with
+    | Var id -> CL_SECVAR id
+    | Const sp -> CL_CONST sp
+    | Ind ind_sp -> CL_IND ind_sp
+    | Prod (_,_,_) -> CL_FUN
+    | Sort _ -> CL_SORT
+    |  _ -> raise Not_found
+
+let rec compute_arguments_scope t =
+  match kind_of_term (Reductionops.whd_betaiotazeta t) with
+    | Prod (_,t,u) ->
+	let sc =
+	  try Some (find_class_scope (find_class t)) with Not_found -> None in
+	sc :: compute_arguments_scope u
+    | _ -> []
+
+let declare_ref_arguments_scope ref =
+  let t = Global.type_of_global ref in
+  declare_arguments_scope ref (compute_arguments_scope t)
+
+(********************************)
+(* Encoding notations as string *)
+
+type symbol =
+  | Terminal of string
+  | NonTerminal of identifier
+  | SProdList of identifier * symbol list
+  | Break of int
+
+let rec string_of_symbol = function
+  | NonTerminal _ -> ["_"]
+  | Terminal s -> [s]
+  | SProdList (_,l) -> 
+     let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"]
+  | Break _ -> []
+
+let make_notation_key symbols =
+  String.concat " " (List.flatten (List.map string_of_symbol symbols))
+
+let decompose_notation_key s =
+  let len = String.length s in
+  let rec decomp_ntn dirs n =
+    if n>=len then dirs else
+    let pos =
+      try
+	String.index_from s n ' ' 
+      with Not_found -> len
+    in
+    let tok =
+      match String.sub s n (pos-n) with
+      | "_" -> NonTerminal (id_of_string "_")
+      | s -> Terminal s in
+    decomp_ntn (tok::dirs) (pos+1)	  
+  in
+    decomp_ntn [] 0
+
+(************)
+(* Printing *)
+
+let pr_delimiters_info = function
+  | None -> str "No delimiting key"
+  | Some key -> str "Delimiting key is " ++ str key
+
+let classes_of_scope sc =
+  Gmap.fold (fun cl sc' l -> if sc = sc' then cl::l else l) !class_scope_map []
+
+let pr_scope_classes sc =
+  let l = classes_of_scope sc in
+  if l = [] then mt()
+  else 
+    hov 0 (str ("Bound to class"^(if List.tl l=[] then "" else "es")) ++
+      spc() ++ prlist_with_sep spc pr_class l) ++ fnl()
+
+let rec rawconstr_of_aconstr () x =
+  rawconstr_of_aconstr_with_binders dummy_loc (fun id () -> (id,())) 
+    rawconstr_of_aconstr () x
+
+let pr_notation_info prraw ntn c =
+  str "\"" ++ str ntn ++ str "\" := " ++ prraw (rawconstr_of_aconstr () c)
+
+let pr_named_scope prraw scope sc =
+ (if scope = default_scope then
+   match Stringmap.fold (fun _ _ x -> x+1) sc.notations 0 with
+     | 0 -> str "No lonely notation"
+     | n -> str "Lonely notation" ++ (if n=1 then mt() else str"s")
+  else 
+    str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
+  ++ fnl ()
+  ++ pr_scope_classes scope
+  ++ Stringmap.fold
+       (fun ntn ((_,r),(_,df),_) strm ->
+	 pr_notation_info prraw df r ++ fnl () ++ strm)
+       sc.notations (mt ())
+
+let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
+
+let pr_scopes prraw =
+ Stringmap.fold 
+   (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
+   !scope_map (mt ())
+
+let rec find_default ntn = function
+  | Scope scope::_ when Stringmap.mem ntn (find_scope scope).notations ->
+      Some scope
+  | SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope
+  | _::scopes -> find_default ntn scopes
+  | [] -> None
+
+let factorize_entries = function
+  | [] -> []
+  | (ntn,c)::l ->
+      let (ntn,l_of_ntn,rest) =
+	List.fold_left
+          (fun (a',l,rest) (a,c) ->
+	    if a = a' then (a',c::l,rest) else (a,[c],(a',l)::rest))
+	  (ntn,[c],[]) l in
+      (ntn,l_of_ntn)::rest
+
+let is_ident s = (* Poor analysis *)
+  String.length s <> 0 & is_letter s.[0]
+
+let browse_notation ntn map =
+  let find =
+    if String.contains ntn ' ' then (=) ntn
+    else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
+  let l =
+    Stringmap.fold 
+      (fun scope_name sc ->
+	Stringmap.fold (fun ntn ((_,r),df,_) l ->
+	  if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
+      map [] in
+  let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in
+  factorize_entries l
+
+let locate_notation prraw ntn =
+  let ntns = browse_notation ntn !scope_map in
+  if ntns = [] then
+    str "Unknown notation"
+  else
+    t (str "Notation            " ++
+    tab () ++ str "Scope     " ++ tab () ++ fnl () ++ 
+    prlist (fun (ntn,l) ->
+      let scope = find_default ntn !scope_stack in
+      prlist 
+	(fun (sc,r,(_,df)) ->
+	  hov 0 (
+	    pr_notation_info prraw df r ++ tbrk (1,2) ++
+	    (if sc = default_scope then mt () else (str ": " ++ str sc)) ++ 
+	    tbrk (1,2) ++
+	    (if Some sc = scope then str "(default interpretation)" else mt ())
+	    ++ fnl ()))
+	l) ntns)
+
+let collect_notation_in_scope scope sc known =
+  assert (scope <> default_scope);
+  Stringmap.fold
+    (fun ntn ((_,r),(_,df),_) (l,known as acc) ->
+      if List.mem ntn known then acc else ((df,r)::l,ntn::known))
+    sc.notations ([],known)
+
+let collect_notations stack =
+  fst (List.fold_left
+    (fun (all,knownntn as acc) -> function
+      | Scope scope ->
+	  if List.mem_assoc scope all then acc
+	  else
+	    let (l,knownntn) =
+	      collect_notation_in_scope scope (find_scope scope) knownntn in
+	    ((scope,l)::all,knownntn)
+      | SingleNotation ntn ->
+	  if List.mem ntn knownntn then (all,knownntn)
+	  else
+	    let ((_,r),(_,df),_) =
+	      Stringmap.find ntn (find_scope default_scope).notations in
+	    let all' = match all with
+	      | (s,lonelyntn)::rest when s = default_scope ->
+		  (s,(df,r)::lonelyntn)::rest
+	      | _ -> 
+		  (default_scope,[df,r])::all in
+	    (all',ntn::knownntn))
+    ([],[]) stack)
+
+let pr_visible_in_scope prraw (scope,ntns) =
+  let strm =
+    List.fold_right
+      (fun (df,r) strm -> pr_notation_info prraw df r ++ fnl () ++ strm)
+      ntns (mt ()) in
+  (if scope = default_scope then
+     str "Lonely notation" ++ (if List.length ntns <> 1 then str "s" else mt())
+   else 
+     str "Visible in scope " ++ str scope)
+  ++ fnl () ++ strm
+
+let pr_scope_stack prraw stack = 
+  List.fold_left
+    (fun strm scntns -> strm ++ pr_visible_in_scope prraw scntns ++ fnl ())
+    (mt ()) (collect_notations stack)
+
+let pr_visibility prraw = function
+  | Some scope -> pr_scope_stack prraw (push_scope scope !scope_stack)
+  | None -> pr_scope_stack prraw !scope_stack
+
+(**********************************************************************)
+(* Mapping notations to concrete syntax *)
+
+type unparsing_rule = unparsing list * precedence
+
+(* Concrete syntax for symbolic-extension table *)
+let printing_rules = 
+  ref (Stringmap.empty : unparsing_rule Stringmap.t)
+
+let declare_notation_printing_rule ntn unpl =
+  printing_rules := Stringmap.add ntn unpl !printing_rules
+
+let find_notation_printing_rule ntn =
+  try Stringmap.find ntn !printing_rules
+  with Not_found -> anomaly ("No printing rule found for "^ntn)
+
+(**********************************************************************)
+(* Synchronisation with reset *)
+
+let freeze () =
+ (!scope_map, !notation_level_map, !scope_stack, !arguments_scope,
+  !delimiters_map, !notations_key_table, !printing_rules,
+  !class_scope_map)
+
+let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
+  scope_map := scm;
+  notation_level_map := nlm;
+  scope_stack := scs;
+  delimiters_map := dlm;
+  arguments_scope := asc;
+  notations_key_table := fkm;
+  printing_rules := pprules;
+  class_scope_map := clsc
+
+let init () =
+  init_scope_map ();
+(*
+  scope_stack := Stringmap.empty
+  arguments_scope := Refmap.empty
+*)
+  notation_level_map := Stringmap.empty;
+  delimiters_map := Stringmap.empty;
+  notations_key_table := Gmapl.empty;
+  printing_rules := Stringmap.empty;
+  class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
+
+let _ = 
+  declare_summary "symbols"
+    { freeze_function = freeze;
+      unfreeze_function = unfreeze;
+      init_function = init;
+      survive_module = false;
+      survive_section = false }
diff --git a/interp/symbols.mli b/interp/symbols.mli
new file mode 100644
index 00000000..00d8e5ff
--- /dev/null
+++ b/interp/symbols.mli
@@ -0,0 +1,160 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: symbols.mli,v 1.22.2.1 2004/07/16 19:30:23 herbelin Exp $ *)
+
+(*i*)
+open Util
+open Pp
+open Bignat
+open Names
+open Nametab
+open Libnames
+open Rawterm
+open Topconstr
+open Ppextend
+
+(*i*)
+
+(**********************************************************************)
+(* Scopes *)
+
+(*s A scope is a set of interpreters for symbols + optional
+   interpreter and printers for integers + optional delimiters *)
+
+type level = precedence * tolerability list
+type delimiters = string
+type scope
+type scopes (* = scope_name list*)
+
+val type_scope : scope_name
+val declare_scope : scope_name -> unit
+
+(* Open scope *)
+
+val current_scopes : unit -> scopes
+val open_close_scope : 
+  (* locality *) bool * (* open *) bool * scope_name -> unit
+
+(* Extend a list of scopes *)
+val empty_scope_stack : scopes
+val push_scope : scope_name -> scopes -> scopes
+
+(* Declare delimiters for printing *)
+
+val declare_delimiters : scope_name -> delimiters -> unit
+val find_delimiters_scope : loc -> delimiters -> scope_name
+
+(*s Declare and uses back and forth a numeral interpretation *)
+
+(* A numeral interpreter is the pair of an interpreter for _integer_
+   numbers in terms and an optional interpreter in pattern, if
+   negative numbers are not supported, the interpreter must fail with
+   an appropriate error message *)
+
+type num_interpreter =
+    (loc -> bigint -> rawconstr)
+    * (loc -> bigint -> name -> cases_pattern) option
+
+type num_uninterpreter =
+    rawconstr list * (rawconstr -> bigint option)
+    * (cases_pattern -> bigint option) option
+
+type required_module = global_reference * string list 
+val declare_numeral_interpreter : scope_name -> required_module ->
+  num_interpreter -> num_uninterpreter -> unit
+
+(* Returns the term/cases_pattern bound to a numeral in a given scope context*)
+val interp_numeral : loc -> bigint -> scope_name list -> rawconstr
+val interp_numeral_as_pattern : loc -> bigint -> name -> scope_name list ->
+  cases_pattern
+
+(* Returns the numeral bound to a term/cases_pattern; raises No_match if no *)
+(* such numeral *)
+val uninterp_numeral : rawconstr -> scope_name * bigint
+val uninterp_cases_numeral : cases_pattern -> scope_name * bigint
+
+val availability_of_numeral : scope_name -> scopes -> delimiters option option
+
+(*s Declare and interpret back and forth a notation *)
+
+(* Binds a notation in a given scope to an interpretation *)
+type interp_rule =
+  | NotationRule of scope_name option * notation
+  | SynDefRule of kernel_name
+val declare_notation_interpretation : notation -> scope_name option ->
+      interpretation -> dir_path * string -> bool -> unit
+
+val declare_uninterpretation : interp_rule -> interpretation -> unit
+
+(* Returns the interpretation bound to a notation *)
+val interp_notation : loc -> notation -> scope_name list -> 
+      interpretation * ((dir_path * string) * scope_name option)
+
+(* Returns the possible notations for a given term *)
+val uninterp_notations : rawconstr ->
+      (interp_rule * interpretation * int option) list
+val uninterp_cases_pattern_notations : cases_pattern ->
+      (interp_rule * interpretation * int option) list
+
+(* Test if a notation is available in the scopes *)
+(* context [scopes] if available, the result is not None; the first *)
+(* argument is itself not None if a delimiters is needed; the second *)
+(* argument is a numeral printer if the *)
+val availability_of_notation : scope_name option * notation -> scopes -> 
+  (scope_name option * delimiters option) option
+
+(*s Declare and test the level of a (possibly uninterpreted) notation *)
+
+val declare_notation_level : notation -> level option * level -> unit
+val level_of_notation : notation -> level option * level 
+      (* raise [Not_found] if no level *)
+
+(*s** Miscellaneous *)
+
+(* Checks for already existing notations *)
+val exists_notation_in_scope : scope_name option -> notation ->
+      interpretation -> bool * bool
+
+(* Declares and looks for scopes associated to arguments of a global ref *)
+val declare_arguments_scope: global_reference -> scope_name option list -> unit
+val find_arguments_scope : global_reference -> scope_name option list
+
+val declare_class_scope : scope_name -> Classops.cl_typ -> unit
+val declare_ref_arguments_scope : global_reference -> unit
+
+val compute_arguments_scope : Term.types -> scope_name option list
+
+(* Building notation key *)
+
+type symbol =
+  | Terminal of string
+  | NonTerminal of identifier
+  | SProdList of identifier * symbol list
+  | Break of int
+
+val make_notation_key : symbol list -> notation
+val decompose_notation_key : notation -> symbol list
+
+(* Prints scopes (expect a pure aconstr printer *)
+val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
+val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
+val locate_notation : (rawconstr -> std_ppcmds) -> notation -> std_ppcmds
+
+val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds
+
+(**********************************************************************)
+(*s Printing rules for notations *)
+
+(* Declare and look for the printing rule for symbolic notations *)
+type unparsing_rule = unparsing list * precedence
+val declare_notation_printing_rule : notation -> unparsing_rule -> unit
+val find_notation_printing_rule : notation -> unparsing_rule
+
+(**********************************************************************)
+(* Rem: printing rules for numerals are trivial *)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
new file mode 100644
index 00000000..ef887d88
--- /dev/null
+++ b/interp/syntax_def.ml
@@ -0,0 +1,75 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: syntax_def.ml,v 1.6.2.1 2004/07/16 19:30:23 herbelin Exp $ *)
+
+open Util
+open Pp
+open Names
+open Libnames
+open Topconstr
+open Libobject
+open Lib
+open Nameops
+
+(* Syntactic definitions. *)
+
+let syntax_table = ref (KNmap.empty : aconstr KNmap.t)
+
+let _ = Summary.declare_summary
+	  "SYNTAXCONSTANT"
+	  { Summary.freeze_function = (fun () -> !syntax_table);
+	    Summary.unfreeze_function = (fun ft -> syntax_table := ft);
+	    Summary.init_function = (fun () -> syntax_table := KNmap.empty);
+	    Summary.survive_module = false;
+	    Summary.survive_section = false }
+
+let add_syntax_constant kn c =
+  syntax_table := KNmap.add kn c !syntax_table
+
+let load_syntax_constant i ((sp,kn),(local,c,onlyparse)) =
+  if Nametab.exists_cci sp then
+    errorlabstrm "cache_syntax_constant"
+      (pr_id (basename sp) ++ str " already exists");
+  add_syntax_constant kn c;
+  Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
+  if not onlyparse then
+    Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
+
+let open_syntax_constant i ((sp,kn),c) =
+  Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn
+
+let cache_syntax_constant d =
+  load_syntax_constant 1 d
+
+let subst_syntax_constant ((sp,kn),subst,(local,c,onlyparse)) =
+  (local,subst_aconstr subst c,onlyparse)
+
+let classify_syntax_constant (_,(local,_,_ as o)) =
+  if local then Dispose else Substitute o
+
+let export_syntax_constant (local,_,_ as o) =
+  if local then None else Some o
+
+let (in_syntax_constant, out_syntax_constant) =
+  declare_object {(default_object "SYNTAXCONSTANT") with
+    cache_function = cache_syntax_constant;
+    load_function = load_syntax_constant;
+    open_function = open_syntax_constant;
+    subst_function = subst_syntax_constant;
+    classify_function = classify_syntax_constant;
+    export_function = export_syntax_constant } 
+
+let declare_syntactic_definition local id onlyparse c =
+  let _ = add_leaf id (in_syntax_constant (local,c,onlyparse)) in ()
+
+let rec set_loc loc _ a =
+  rawconstr_of_aconstr_with_binders loc (fun id e -> (id,e)) (set_loc loc) () a
+
+let search_syntactic_definition loc kn =
+  set_loc loc () (KNmap.find kn !syntax_table)
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
new file mode 100644
index 00000000..0aec03c2
--- /dev/null
+++ b/interp/syntax_def.mli
@@ -0,0 +1,25 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: syntax_def.mli,v 1.3.2.2 2004/07/16 19:30:23 herbelin Exp $ i*)
+
+(*i*)
+open Util
+open Names
+open Topconstr
+open Rawterm
+(*i*)
+
+(* Syntactic definitions. *)
+
+val declare_syntactic_definition : bool -> identifier -> bool -> aconstr
+  -> unit
+
+val search_syntactic_definition : loc -> kernel_name -> rawconstr
+
+
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
new file mode 100644
index 00000000..3ee3285b
--- /dev/null
+++ b/interp/topconstr.ml
@@ -0,0 +1,702 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: topconstr.ml,v 1.35.2.2 2004/07/16 19:30:23 herbelin Exp $ *)
+
+(*i*)
+open Pp
+open Util
+open Names
+open Nameops
+open Libnames
+open Rawterm
+open Term
+(*i*)
+
+(**********************************************************************)
+(* This is the subtype of rawconstr allowed in syntactic extensions *)
+
+(* For AList: first constr is iterator, second is terminator;
+   first id is where each argument of the list has to be substituted 
+   in iterator and snd id is alternative name just for printing;
+   boolean is associativity *)
+
+type aconstr =
+  (* Part common to rawconstr and cases_pattern *)
+  | ARef of global_reference
+  | AVar of identifier
+  | AApp of aconstr * aconstr list
+  | AList of identifier * identifier * aconstr * aconstr * bool
+  (* Part only in rawconstr *)
+  | ALambda of name * aconstr * aconstr
+  | AProd of name * aconstr * aconstr
+  | ALetIn of name * aconstr * aconstr
+  | ACases of aconstr option * aconstr option *
+      (aconstr * (name * (inductive * name list) option)) list *
+      (identifier list * cases_pattern list * aconstr) list
+  | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
+  | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
+  | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
+  | ASort of rawsort
+  | AHole of hole_kind
+  | APatVar of patvar
+  | ACast of aconstr * aconstr
+  
+let name_app f e = function
+  | Name id -> let (id, e) = f id e in (Name id, e)
+  | Anonymous -> Anonymous, e
+
+let rec subst_rawvars l = function
+  | RVar (_,id) as r -> (try List.assoc id l with Not_found -> r)
+  | r -> map_rawconstr (subst_rawvars l) r (* assume: id is not binding *)
+
+let ldots_var = id_of_string ".."
+
+let rawconstr_of_aconstr_with_binders loc g f e = function
+  | AVar id -> RVar (loc,id)
+  | AApp (a,args) -> RApp (loc,f e a, List.map (f e) args)
+  | AList (x,y,iter,tail,swap) ->
+      let t = f e tail in let it = f e iter in
+      let innerl = (ldots_var,t)::(if swap then [] else [x,RVar(loc,y)]) in
+      let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in
+      let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in
+      subst_rawvars outerl it
+  | ALambda (na,ty,c) ->
+      let na,e = name_app g e na in RLambda (loc,na,f e ty,f e c)
+  | AProd (na,ty,c) ->
+      let na,e = name_app g e na in RProd (loc,na,f e ty,f e c)
+  | ALetIn (na,b,c) ->
+      let na,e = name_app g e na in RLetIn (loc,na,f e b,f e c)
+  | ACases (tyopt,rtntypopt,tml,eqnl) ->
+      let cases_predicate_names tml =
+	List.flatten (List.map (function
+	  | (tm,(na,None)) -> [na]
+	  | (tm,(na,Some (_,nal))) -> na::nal) tml) in
+      (* TODO: apply g to na (in fact not used) *)
+      let e' = List.fold_right
+	(fun na e -> snd (name_app g e na)) (cases_predicate_names tml) e in
+      let fold id (idl,e) = let (id,e) = g id e in (id::idl,e) in
+      let eqnl = List.map (fun (idl,pat,rhs) ->
+        let (idl,e) = List.fold_right fold idl ([],e) in (loc,idl,pat,f e rhs)) eqnl in
+      RCases (loc,(option_app (f e) tyopt, ref (option_app (f e') rtntypopt)),
+        List.map (fun (tm,(na,x)) -> 
+	  (f e tm,ref (na,option_app (fun (x,y) -> (loc,x,y)) x))) tml,eqnl)
+  | AOrderedCase (b,tyopt,tm,bv) ->
+      ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv,ref None)
+  | ALetTuple (nal,(na,po),b,c) ->
+      RLetTuple (loc,nal,(na,option_app (f e) po),f e b,f e c)
+  | AIf (c,(na,po),b1,b2) ->
+      RIf (loc,f e c,(na,option_app (f e) po),f e b1,f e b2)
+  | ACast (c,t) -> RCast (loc,f e c,f e t)
+  | ASort x -> RSort (loc,x)
+  | AHole x  -> RHole (loc,x)
+  | APatVar n -> RPatVar (loc,(false,n))
+  | ARef x -> RRef (loc,x)
+
+let rec subst_pat subst pat = 
+  match pat with
+  | PatVar _ -> pat
+  | PatCstr (loc,((kn,i),j),cpl,n) -> 
+      let kn' = subst_kn subst kn 
+      and cpl' = list_smartmap (subst_pat subst) cpl in
+        if kn' == kn && cpl' == cpl then pat else
+          PatCstr (loc,((kn',i),j),cpl',n)
+
+let rec subst_aconstr subst raw =
+  match raw with
+  | ARef ref -> 
+      let ref' = subst_global subst ref in 
+	if ref' == ref then raw else
+	  ARef ref'
+
+  | AVar _ -> raw
+
+  | AApp (r,rl) -> 
+      let r' = subst_aconstr subst r 
+      and rl' = list_smartmap (subst_aconstr subst) rl in
+	if r' == r && rl' == rl then raw else
+	  AApp(r',rl')
+
+  | AList (id1,id2,r1,r2,b) -> 
+      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  AList (id1,id2,r1',r2',b)
+
+  | ALambda (n,r1,r2) -> 
+      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  ALambda (n,r1',r2')
+
+  | AProd (n,r1,r2) -> 
+      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  AProd (n,r1',r2')
+
+  | ALetIn (n,r1,r2) -> 
+      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  ALetIn (n,r1',r2')
+
+  | ACases (ro,rtntypopt,rl,branches) -> 
+      let ro' = option_smartmap (subst_aconstr subst) ro 
+      and rtntypopt' = option_smartmap (subst_aconstr subst) rtntypopt
+      and rl' = list_smartmap
+        (fun (a,(n,signopt) as x) -> 
+	  let a' = subst_aconstr subst a in
+	  let signopt' = option_app (fun ((indkn,i),nal as z) ->
+	    let indkn' = subst_kn subst indkn in
+	    if indkn == indkn' then z else ((indkn',i),nal)) signopt in
+	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
+        rl
+      and branches' = list_smartmap 
+                        (fun (idl,cpl,r as branch) ->
+                           let cpl' = list_smartmap (subst_pat subst) cpl
+                           and r' = subst_aconstr subst r in
+                             if cpl' == cpl && r' == r then branch else
+                               (idl,cpl',r'))
+                        branches
+      in
+        if ro' == ro && rtntypopt == rtntypopt' &
+          rl' == rl && branches' == branches then raw else
+          ACases (ro',rtntypopt',rl',branches')
+
+  | AOrderedCase (b,ro,r,ra) -> 
+      let ro' = option_smartmap (subst_aconstr subst) ro
+      and r' = subst_aconstr subst r 
+      and ra' = array_smartmap (subst_aconstr subst) ra in
+	if ro' == ro && r' == r && ra' == ra then raw else
+	  AOrderedCase (b,ro',r',ra')
+
+  | ALetTuple (nal,(na,po),b,c) ->
+      let po' = option_smartmap (subst_aconstr subst) po
+      and b' = subst_aconstr subst b 
+      and c' = subst_aconstr subst c in
+	if po' == po && b' == b && c' == c then raw else
+	  ALetTuple (nal,(na,po'),b',c')
+
+  | AIf (c,(na,po),b1,b2) ->
+      let po' = option_smartmap (subst_aconstr subst) po
+      and b1' = subst_aconstr subst b1
+      and b2' = subst_aconstr subst b2 
+      and c' = subst_aconstr subst c in
+	if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
+	  AIf (c',(na,po'),b1',b2')
+
+  | APatVar _ | ASort _ -> raw
+
+  | AHole (ImplicitArg (ref,i)) ->
+      let ref' = subst_global subst ref in 
+	if ref' == ref then raw else
+	  AHole (ImplicitArg (ref',i))
+  | AHole (BinderType _ | QuestionMark | CasesType |
+      InternalHole | TomatchTypeParameter _) -> raw
+
+  | ACast (r1,r2) -> 
+      let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
+	if r1' == r1 && r2' == r2 then raw else
+	  ACast (r1',r2')
+
+let add_name r = function
+  | Anonymous -> ()
+  | Name id -> r := id :: !r
+
+let has_ldots =
+  List.exists
+    (function RApp (_,RVar(_,v),_) when v = ldots_var -> true | _ -> false)
+
+let compare_rawconstr f t1 t2 = match t1,t2 with
+  | RRef (_,r1), RRef (_,r2) -> r1 = r2
+  | RVar (_,v1), RVar (_,v2) -> v1 = v2
+  | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & List.for_all2 f l1 l2
+  | RLambda (_,na1,ty1,c1), RLambda (_,na2,ty2,c2) when na1 = na2 ->
+      f ty1 ty2 & f c1 c2
+  | RProd (_,na1,ty1,c1), RProd (_,na2,ty2,c2) when na1 = na2 ->
+      f ty1 ty2 & f c1 c2
+  | RHole _, RHole _ -> true
+  | RSort (_,s1), RSort (_,s2) -> s1 = s2
+  | (RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _
+    | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
+  | _,(RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _
+      | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
+      -> error "Unsupported construction in recursive notations"
+  | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
+      -> false
+
+let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr t1 t2
+
+let discriminate_patterns nl l1 l2 =
+  let diff = ref None in
+  let rec aux n c1 c2 = match c1,c2 with
+  | RVar (_,v1), RVar (_,v2) when v1<>v2 ->
+      if !diff = None then (diff := Some (v1,v2,(n>=nl)); true)
+      else 
+        !diff = Some (v1,v2,(n>=nl)) or !diff = Some (v2,v1,(n<nl))
+        or (error
+          "Both ends of the recursive pattern differ in more than one place")
+  | _ -> compare_rawconstr (aux (n+1)) c1 c2 in
+  let l = list_map2_i aux 0 l1 l2 in
+  if not (List.for_all ((=) true) l) then
+    error "Both ends of the recursive pattern differ";
+  !diff
+
+let aconstr_and_vars_of_rawconstr a =
+  let found = ref [] in
+  let bound_binders = ref [] in
+  let rec aux = function
+  | RVar (_,id) -> 
+      if not (List.mem id !bound_binders) then found := id::!found;
+      AVar id
+  | RApp (_,f,args) when has_ldots args -> make_aconstr_list f args 
+  | RApp (_,g,args) -> AApp (aux g, List.map aux args)
+  | RLambda (_,na,ty,c) -> add_name bound_binders na; ALambda (na,aux ty,aux c)
+  | RProd (_,na,ty,c) -> add_name bound_binders na; AProd (na,aux ty,aux c)
+  | RLetIn (_,na,b,c) -> add_name bound_binders na; ALetIn (na,aux b,aux c)
+  | RCases (_,(tyopt,rtntypopt),tml,eqnl) ->
+      let f (_,idl,pat,rhs) =
+        bound_binders := idl@(!bound_binders);
+        (idl,pat,aux rhs) in
+      ACases (option_app aux tyopt,
+        option_app aux !rtntypopt,
+        List.map (fun (tm,{contents = (na,x)}) ->
+	  add_name bound_binders na;
+	  option_iter
+	    (fun (_,_,nl) -> List.iter (add_name bound_binders) nl) x;
+          (aux tm,(na,option_app (fun (_,ind,nal) -> (ind,nal)) x))) tml,
+        List.map f eqnl)
+  | ROrderedCase (_,b,tyopt,tm,bv,_) ->
+      AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
+  | RLetTuple (loc,nal,(na,po),b,c) ->
+      ALetTuple (nal,(na,option_app aux po),aux b,aux c)
+  | RIf (loc,c,(na,po),b1,b2) ->
+      AIf (aux c,(na,option_app aux po),aux b1,aux b2)
+  | RCast (_,c,t) -> ACast (aux c,aux t)
+  | RSort (_,s) -> ASort s
+  | RHole (_,w) -> AHole w
+  | RRef (_,r) -> ARef r
+  | RPatVar (_,(_,n)) -> APatVar n
+  | RDynamic _ | RRec _ | REvar _ ->
+      error "Fixpoints, cofixpoints, existential variables and pattern-matching  not \
+allowed in abbreviatable expressions"
+
+  (* Recognizing recursive notations *)
+  and terminator_of_pat f1 ll1 lr1 = function
+  | RApp (loc,f2,l2) ->
+      if not (eq_rawconstr f1 f2) then error
+	"Cannot recognize the same head to both ends of the recursive pattern";
+      let nl = List.length ll1 in
+      let nr = List.length lr1 in
+      if List.length l2 <> nl + nr + 1 then
+	error "Both ends of the recursive pattern have different lengths";
+      let ll2,l2' = list_chop nl l2 in
+      let t = List.hd l2' and lr2 = List.tl l2' in
+      let discr = discriminate_patterns nl (ll1@lr1) (ll2@lr2) in
+      let x,y,order = match discr with Some z -> z | None -> 
+	error "Both ends of the recursive pattern are the same" in
+      List.iter (fun id ->
+        if List.mem id !bound_binders or List.mem id !found 
+        then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part";
+        found := id::!found) [x;y];
+      let iter =
+        if order then RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2)
+        else RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1) in
+      (if order then y else x),(if order then x else y), aux iter, aux t, order
+  | _ -> error "One end of the recursive pattern is not an application"
+    
+  and make_aconstr_list f args =
+    let rec find_patterns acc = function
+      | RApp(_,RVar (_,a),[c]) :: l when a = ldots_var ->
+          (* We've found the recursive part *)
+	  let x,y,iter,term,lassoc = terminator_of_pat f (List.rev acc) l c in
+	  AList (x,y,iter,term,lassoc)
+      | a::l -> find_patterns (a::acc) l
+      | [] -> error "Ill-formed recursive notation"
+    in find_patterns [] args
+
+  in
+  let t = aux a in
+  (* Side effect *)
+  t, !found, !bound_binders
+
+let aconstr_of_rawconstr vars a =
+  let a,notbindingvars,binders = aconstr_and_vars_of_rawconstr a in
+  let check_type x =
+    if not (List.mem x notbindingvars or List.mem x binders) then
+      error ((string_of_id x)^" is unbound in the right-hand-side") in
+  List.iter check_type vars;
+  a
+
+let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
+
+(* Pattern-matching rawconstr and aconstr *)
+
+let rec adjust_scopes = function
+  | _,[] -> []
+  | [],a::args -> (None,a) :: adjust_scopes ([],args)
+  | sc::scopes,a::args -> (sc,a) :: adjust_scopes (scopes,args)
+
+exception No_match
+
+let rec alpha_var id1 id2 = function
+  | (i1,i2)::_ when i1=id1 -> i2 = id2
+  | (i1,i2)::_ when i2=id2 -> i1 = id1
+  | _::idl -> alpha_var id1 id2 idl
+  | [] -> id1 = id2
+
+let alpha_eq_val (x,y) = x = y
+
+let bind_env sigma var v =
+  try
+    let vvar = List.assoc var sigma in
+    if alpha_eq_val (v,vvar) then sigma
+    else raise No_match
+  with Not_found ->
+    (* TODO: handle the case of multiple occs in different scopes *)
+    (var,v)::sigma
+
+let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
+  | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
+  | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
+  | RRef (_,r1), ARef r2 when r1 = r2 -> sigma
+  | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
+  | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 ->
+      List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2
+  | RApp (_,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc) 
+      when List.length l1 = List.length l2 ->
+      match_alist alp metas sigma (f1::l1) (f2::l2) x iter termin lassoc
+  | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) ->
+     match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
+  | RProd (_,na1,t1,b1), AProd (na2,t2,b2) ->
+     match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
+  | RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) ->
+     match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
+  | RCases (_,(po1,rtno1),tml1,eqnl1), ACases (po2,rtno2,tml2,eqnl2) 
+      when List.length tml1 = List.length tml2 ->
+     let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in
+     (* TODO: match rtno' with their contexts *)
+     let sigma = List.fold_left2 
+       (fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in
+     List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2
+  | ROrderedCase (_,st,po1,c1,bl1,_), AOrderedCase (st2,po2,c2,bl2) 
+      when Array.length bl1 = Array.length bl2 ->
+     let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in
+     array_fold_left2 (match_ alp metas) (match_ alp metas sigma c1 c2) bl1 bl2
+  | RCast(_,c1,t1), ACast(c2,t2) ->
+      match_ alp metas (match_ alp metas sigma c1 c2) t1 t2
+  | RSort (_,s1), ASort s2 when s1 = s2 -> sigma
+  | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
+  | a, AHole _ when not(Options.do_translate()) -> sigma
+  | RHole _, AHole _ -> sigma
+  | (RDynamic _ | RRec _ | REvar _), _ 
+  | _,_ -> raise No_match
+
+and match_alist alp metas sigma l1 l2 x iter termin lassoc =
+  (* match the iterator at least once *)
+  let sigma = List.fold_left2 (match_ alp (ldots_var::metas)) sigma l1 l2 in
+  (* Recover the recursive position *)
+  let rest = List.assoc ldots_var sigma in
+  (* Recover the first element *)
+  let t1 = List.assoc x sigma in
+  let sigma = List.remove_assoc x (List.remove_assoc ldots_var sigma) in
+  (* try to find the remaining elements or the terminator *)
+  let rec match_alist_tail alp metas sigma acc rest =
+    try 
+      let sigma = match_ alp (ldots_var::metas) sigma rest iter in
+      let rest = List.assoc ldots_var sigma in
+      let t = List.assoc x sigma in
+      let sigma = List.remove_assoc x (List.remove_assoc ldots_var sigma) in
+      match_alist_tail alp metas sigma (t::acc) rest
+    with No_match ->
+      List.rev acc, match_ alp metas sigma rest termin in
+  let tl,sigma = match_alist_tail alp metas sigma [t1] rest in
+  (x,encode_list_value (if lassoc then List.rev tl else tl))::sigma
+
+and match_binders alp metas sigma b1 b2 na1 na2 = match (na1,na2) with
+  | (Name id1,Name id2) when List.mem id2 metas ->
+      let sigma = bind_env sigma id2 (RVar (dummy_loc,id1)) in 
+      match_ alp metas sigma b1 b2
+  | (Name id1,Name id2) -> match_ ((id1,id2)::alp) metas sigma b1 b2
+  | (Anonymous,Anonymous) -> match_  alp metas sigma b1 b2
+  | _ -> raise No_match
+
+and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) =
+  if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then
+    match_ alp metas sigma rhs1 rhs2
+  else raise No_match
+
+type scope_name = string
+
+type interpretation = 
+    (identifier * (scope_name option * scope_name list)) list * aconstr
+
+let match_aconstr c (metas_scl,pat) =
+  let subst = match_ [] (List.map fst metas_scl) [] c pat in
+  (* Reorder canonically the substitution *)
+  let find x subst =
+    try List.assoc x subst
+    with Not_found ->
+      (* Happens for binders bound to Anonymous *)
+      (* Find a better way to propagate Anonymous... *)
+      RVar (dummy_loc,x) in
+  List.map (fun (x,scl) -> (find x subst,scl)) metas_scl
+
+(**********************************************************************)
+(*s Concrete syntax for terms *)
+
+type notation = string
+
+type explicitation = ExplByPos of int | ExplByName of identifier
+
+type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
+
+type cases_pattern_expr =
+  | CPatAlias of loc * cases_pattern_expr * identifier
+  | CPatCstr of loc * reference * cases_pattern_expr list
+  | CPatAtom of loc * reference option
+  | CPatNotation of loc * notation * cases_pattern_expr list
+  | CPatNumeral of loc * Bignat.bigint
+  | CPatDelimiters of loc * string * cases_pattern_expr
+
+type constr_expr =
+  | CRef of reference
+  | CFix of loc * identifier located * fixpoint_expr list
+  | CCoFix of loc * identifier located * cofixpoint_expr list
+  | CArrow of loc * constr_expr * constr_expr
+  | CProdN of loc * (name located list * constr_expr) list * constr_expr
+  | CLambdaN of loc * (name located list * constr_expr) list * constr_expr
+  | CLetIn of loc * name located * constr_expr * constr_expr
+  | CAppExpl of loc * (proj_flag * reference) * constr_expr list
+  | CApp of loc * (proj_flag * constr_expr) * 
+      (constr_expr * explicitation located option) list
+  | CCases of loc * (constr_expr option * constr_expr option) *
+      (constr_expr * (name option * constr_expr option)) list *
+      (loc * cases_pattern_expr list * constr_expr) list
+  | COrderedCase of loc * case_style * constr_expr option * constr_expr
+      * constr_expr list
+  | CLetTuple of loc * name list * (name option * constr_expr option) *
+      constr_expr * constr_expr
+  | CIf of loc * constr_expr * (name option * constr_expr option)
+      * constr_expr * constr_expr
+  | CHole of loc
+  | CPatVar of loc * (bool * patvar)
+  | CEvar of loc * existential_key
+  | CSort of loc * rawsort
+  | CCast of loc * constr_expr * constr_expr
+  | CNotation of loc * notation * constr_expr list
+  | CNumeral of loc * Bignat.bigint
+  | CDelimiters of loc * string * constr_expr
+  | CDynamic of loc * Dyn.t
+
+and fixpoint_expr =
+    identifier * int * local_binder list * constr_expr * constr_expr
+
+and local_binder =
+  | LocalRawDef of name located * constr_expr
+  | LocalRawAssum of name located list * constr_expr
+
+and cofixpoint_expr =
+    identifier * local_binder list * constr_expr * constr_expr
+
+(***********************)
+(* For binders parsing *)
+
+let rec local_binders_length = function
+  | [] -> 0
+  | LocalRawDef _::bl -> 1 + local_binders_length bl
+  | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
+
+let names_of_local_assums bl =
+  List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl)
+
+(**********************************************************************)
+(* Functions on constr_expr *)
+
+let constr_loc = function
+  | CRef (Ident (loc,_)) -> loc
+  | CRef (Qualid (loc,_)) -> loc
+  | CFix (loc,_,_) -> loc
+  | CCoFix (loc,_,_) -> loc
+  | CArrow (loc,_,_) -> loc
+  | CProdN (loc,_,_) -> loc
+  | CLambdaN (loc,_,_) -> loc
+  | CLetIn (loc,_,_,_) -> loc
+  | CAppExpl (loc,_,_) -> loc
+  | CApp (loc,_,_) -> loc
+  | CCases (loc,_,_,_) -> loc
+  | COrderedCase (loc,_,_,_,_) -> loc
+  | CLetTuple (loc,_,_,_,_) -> loc
+  | CIf (loc,_,_,_,_) -> loc
+  | CHole loc -> loc
+  | CPatVar (loc,_) -> loc
+  | CEvar (loc,_) -> loc
+  | CSort (loc,_) -> loc
+  | CCast (loc,_,_) -> loc
+  | CNotation (loc,_,_) -> loc
+  | CNumeral (loc,_) -> loc
+  | CDelimiters (loc,_,_) -> loc
+  | CDynamic _ -> dummy_loc
+
+let cases_pattern_loc = function
+  | CPatAlias (loc,_,_) -> loc
+  | CPatCstr (loc,_,_) -> loc
+  | CPatAtom (loc,_) -> loc
+  | CPatNotation (loc,_,_) -> loc
+  | CPatNumeral (loc,_) -> loc
+  | CPatDelimiters (loc,_,_) -> loc
+
+let occur_var_constr_ref id = function
+  | Ident (loc,id') -> id = id'
+  | Qualid _ -> false
+
+let rec occur_var_constr_expr id = function
+  | CRef r -> occur_var_constr_ref id r
+  | CArrow (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b
+  | CAppExpl (loc,(_,r),l) ->
+      occur_var_constr_ref id r or List.exists (occur_var_constr_expr id) l
+  | CApp (loc,(_,f),l) ->
+      occur_var_constr_expr id f or
+      List.exists (fun (a,_) -> occur_var_constr_expr id a) l
+  | CProdN (_,l,b) -> occur_var_binders id b l
+  | CLambdaN (_,l,b) -> occur_var_binders id b l
+  | CLetIn (_,na,a,b) -> occur_var_binders id b [[na],a]
+  | CCast (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b
+  | CNotation (_,_,l) -> List.exists (occur_var_constr_expr id) l
+  | CDelimiters (loc,_,a) -> occur_var_constr_expr id a
+  | CHole _ | CEvar _ | CPatVar _ | CSort _ | CNumeral _ | CDynamic _ -> false
+  | CCases (loc,_,_,_) 
+  | COrderedCase (loc,_,_,_,_) 
+  | CLetTuple (loc,_,_,_,_) 
+  | CIf (loc,_,_,_,_) 
+  | CFix (loc,_,_) 
+  | CCoFix (loc,_,_) -> 
+      Pp.warning "Capture check in multiple binders not done"; false
+
+and occur_var_binders id b = function
+  | (idl,a)::l -> 
+      occur_var_constr_expr id a or
+      (not (List.mem (Name id) (snd (List.split idl)))
+      & occur_var_binders id b l)
+  | [] -> occur_var_constr_expr id b
+
+let mkIdentC id  = CRef (Ident (dummy_loc, id))
+let mkRefC r     = CRef r
+let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l)
+let mkCastC (a,b)  = CCast (dummy_loc,a,b)
+let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b)
+let mkLetInC (id,a,b)   = CLetIn (dummy_loc,id,a,b)
+let mkProdC (idl,a,b)   = CProdN (dummy_loc,[idl,a],b)
+
+(* Used in correctness and interface *)
+
+
+let names_of_cases_indtype =
+  let rec vars_of ids t =
+    match t with
+      (* We deal only with the regular cases *)
+      | CApp (_,_,l) -> List.fold_left (fun ids (a,_) -> vars_of ids a) [] l
+      | CRef (Ident (_,id)) -> id::ids
+      | CNotation (_,_,l)
+      (* assume the ntn is applicative and does not instantiate the head !! *)
+      | CAppExpl (_,_,l) -> List.fold_left vars_of [] l
+      | CDelimiters(_,_,c) -> vars_of ids c
+      | _ -> ids in
+  vars_of []
+
+let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
+
+let map_binders f g e bl =
+  (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
+  let h (e,bl) (nal,t) = (map_binder g e nal,(nal,f e t)::bl) in
+  let (e,rbl) = List.fold_left h (e,[]) bl in
+  (e, List.rev rbl)
+
+let map_local_binders f g e bl =
+  (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
+  let h (e,bl) = function
+      LocalRawAssum(nal,ty) ->
+        (map_binder g e nal, LocalRawAssum(nal,f e ty)::bl)
+    | LocalRawDef((loc,na),ty) ->
+        (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) in
+  let (e,rbl) = List.fold_left h (e,[]) bl in
+  (e, List.rev rbl)
+
+let map_constr_expr_with_binders f g e = function
+  | CArrow (loc,a,b) -> CArrow (loc,f e a,f e b)
+  | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l) 
+  | CApp (loc,(p,a),l) -> 
+      CApp (loc,(p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
+  | CProdN (loc,bl,b) ->
+      let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b)
+  | CLambdaN (loc,bl,b) ->
+      let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b)
+  | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b)
+  | CCast (loc,a,b) -> CCast (loc,f e a,f e b)
+  | CNotation (loc,n,l) -> CNotation (loc,n,List.map (f e) l)
+  | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
+  | CHole _ | CEvar _ | CPatVar _ | CSort _ 
+  | CNumeral _ | CDynamic _ | CRef _ as x -> x
+  | CCases (loc,(po,rtnpo),a,bl) ->
+      (* TODO: apply g on the binding variables in pat... *)
+      let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
+      let e' = 
+	List.fold_right
+	  (fun (tm,(na,indnal)) e ->
+	    option_fold_right
+	      (fun t ->
+		let ids = names_of_cases_indtype t in
+		List.fold_right g ids)
+            indnal (option_fold_right (name_fold g) na e))
+	  a e
+      in
+      CCases (loc,(option_app (f e) po, option_app (f e') rtnpo),
+         List.map (fun (tm,x) -> (f e tm,x)) a,bl)
+  | COrderedCase (loc,s,po,a,bl) ->
+      COrderedCase (loc,s,option_app (f e) po,f e a,List.map (f e) bl)
+  | CLetTuple (loc,nal,(ona,po),b,c) ->
+      let e' = List.fold_right (name_fold g) nal e in
+      let e'' = option_fold_right (name_fold g) ona e in
+      CLetTuple (loc,nal,(ona,option_app (f e'') po),f e b,f e' c)
+  | CIf (loc,c,(ona,po),b1,b2) ->
+      let e' = option_fold_right (name_fold g) ona e in
+      CIf (loc,f e c,(ona,option_app (f e') po),f e b1,f e b2)
+  | CFix (loc,id,dl) ->
+      CFix (loc,id,List.map (fun (id,n,bl,t,d) -> 
+        let (e',bl') = map_local_binders f g e bl in
+        let t' = f e' t in
+        (* Note: fix names should be inserted before the arguments... *)
+        let e'' = List.fold_left (fun e (id,_,_,_,_) -> g id e) e' dl in
+        let d' = f e'' d in
+        (id,n,bl',t',d')) dl)
+  | CCoFix (loc,id,dl) ->
+      CCoFix (loc,id,List.map (fun (id,bl,t,d) ->
+        let (e',bl') = map_local_binders f g e bl in
+        let t' = f e' t in
+        let e'' = List.fold_left (fun e (id,_,_,_) -> g id e) e' dl in
+        let d' = f e'' d in
+        (id,bl',t',d')) dl)
+
+(* Used in constrintern *)
+let rec replace_vars_constr_expr l = function
+  | CRef (Ident (loc,id)) as x ->
+      (try CRef (Ident (loc,List.assoc id l)) with Not_found -> x)
+  | c -> map_constr_expr_with_binders replace_vars_constr_expr 
+      (fun id l -> List.remove_assoc id l) l c
+
+(**********************************************************************)
+(* Concrete syntax for modules and modules types *)
+
+type with_declaration_ast = 
+  | CWith_Module of identifier located * qualid located
+  | CWith_Definition of identifier located * constr_expr
+
+type module_type_ast = 
+  | CMTEident of qualid located
+  | CMTEwith of module_type_ast * with_declaration_ast
+
+type module_ast = 
+  | CMEident of qualid located
+  | CMEapply of module_ast * module_ast
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
new file mode 100644
index 00000000..f4a82a3a
--- /dev/null
+++ b/interp/topconstr.mli
@@ -0,0 +1,172 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: topconstr.mli,v 1.23.2.1 2004/07/16 19:30:23 herbelin Exp $ *)
+
+(*i*)
+open Pp
+open Util
+open Names
+open Libnames
+open Rawterm
+open Term
+(*i*)
+
+(*s This is the subtype of rawconstr allowed in syntactic extensions *)
+(* No location since intended to be substituted at any place of a text *)
+(* Complex expressions such as fixpoints and cofixpoints are excluded, *)
+(* non global expressions such as existential variables also *)
+
+type aconstr =
+  (* Part common to rawconstr and cases_pattern *)
+  | ARef of global_reference
+  | AVar of identifier
+  | AApp of aconstr * aconstr list
+  | AList of identifier * identifier * aconstr * aconstr * bool
+  (* Part only in rawconstr *)
+  | ALambda of name * aconstr * aconstr
+  | AProd of name * aconstr * aconstr
+  | ALetIn of name * aconstr * aconstr
+  | ACases of aconstr option * aconstr option *
+      (aconstr * (name * (inductive * name list) option)) list *
+      (identifier list * cases_pattern list * aconstr) list
+  | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
+  | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
+  | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
+  | ASort of rawsort
+  | AHole of hole_kind
+  | APatVar of patvar
+  | ACast of aconstr * aconstr
+
+val rawconstr_of_aconstr_with_binders : loc -> 
+  (identifier -> 'a -> identifier * 'a) ->
+  ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
+
+val subst_aconstr : Names.substitution -> aconstr -> aconstr
+
+val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
+
+(* [match_aconstr metas] match a rawconstr against an aconstr with
+   metavariables in [metas]; it raises [No_match] if the matching fails *)
+exception No_match
+
+type scope_name = string
+type interpretation = 
+    (identifier * (scope_name option * scope_name list)) list * aconstr
+
+val match_aconstr : (* scope_name option -> *) rawconstr -> interpretation ->
+      (rawconstr * (scope_name option * scope_name list)) list
+
+(*s Concrete syntax for terms *)
+
+type notation = string
+
+type explicitation = ExplByPos of int | ExplByName of identifier
+
+type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
+
+type cases_pattern_expr =
+  | CPatAlias of loc * cases_pattern_expr * identifier
+  | CPatCstr of loc * reference * cases_pattern_expr list
+  | CPatAtom of loc * reference option
+  | CPatNotation of loc * notation * cases_pattern_expr list
+  | CPatNumeral of loc * Bignat.bigint
+  | CPatDelimiters of loc * string * cases_pattern_expr
+
+type constr_expr =
+  | CRef of reference
+  | CFix of loc * identifier located * fixpoint_expr list
+  | CCoFix of loc * identifier located * cofixpoint_expr list
+  | CArrow of loc * constr_expr * constr_expr
+  | CProdN of loc * (name located list * constr_expr) list * constr_expr
+  | CLambdaN of loc * (name located list * constr_expr) list * constr_expr
+  | CLetIn of loc * name located * constr_expr * constr_expr
+  | CAppExpl of loc * (proj_flag * reference) * constr_expr list
+  | CApp of loc * (proj_flag * constr_expr) * 
+        (constr_expr * explicitation located option) list
+  | CCases of loc * (constr_expr option * constr_expr option) *
+      (constr_expr * (name option * constr_expr option)) list *
+      (loc * cases_pattern_expr list * constr_expr) list
+  | COrderedCase of loc * case_style * constr_expr option * constr_expr
+      * constr_expr list
+  | CLetTuple of loc * name list * (name option * constr_expr option) *
+      constr_expr * constr_expr
+  | CIf of loc * constr_expr * (name option * constr_expr option)
+      * constr_expr * constr_expr
+  | CHole of loc
+  | CPatVar of loc * (bool * patvar)
+  | CEvar of loc * existential_key
+  | CSort of loc * rawsort
+  | CCast of loc * constr_expr * constr_expr
+  | CNotation of loc * notation * constr_expr list
+  | CNumeral of loc * Bignat.bigint
+  | CDelimiters of loc * string * constr_expr
+  | CDynamic of loc * Dyn.t
+
+and fixpoint_expr =
+    identifier * int * local_binder list * constr_expr * constr_expr
+
+and cofixpoint_expr =
+    identifier * local_binder list * constr_expr * constr_expr
+
+and local_binder =
+  | LocalRawDef of name located * constr_expr
+  | LocalRawAssum of name located list * constr_expr
+
+
+val constr_loc : constr_expr -> loc
+
+val cases_pattern_loc : cases_pattern_expr -> loc
+
+val replace_vars_constr_expr :
+  (identifier * identifier) list -> constr_expr -> constr_expr
+
+val occur_var_constr_expr : identifier -> constr_expr -> bool
+
+(* Specific function for interning "in indtype" syntax of "match" *)
+val names_of_cases_indtype : constr_expr -> identifier list
+
+val mkIdentC : identifier -> constr_expr
+val mkRefC : reference -> constr_expr
+val mkAppC : constr_expr * constr_expr list -> constr_expr
+val mkCastC : constr_expr * constr_expr -> constr_expr
+val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
+val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
+val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
+
+(* For binders parsing *)
+
+(* Includes let binders *)
+val local_binders_length : local_binder list -> int
+
+(* Does not take let binders into account *)
+val names_of_local_assums : local_binder list -> name located list
+
+(* Used in correctness and interface; absence of var capture not guaranteed *)
+(* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
+
+val map_constr_expr_with_binders :
+  ('a -> constr_expr -> constr_expr) ->
+      (identifier -> 'a -> 'a) -> 'a -> constr_expr -> constr_expr
+
+(* Concrete syntax for modules and modules types *)
+
+type with_declaration_ast = 
+  | CWith_Module of identifier located * qualid located
+  | CWith_Definition of identifier located * constr_expr
+
+type module_type_ast = 
+  | CMTEident of qualid located
+  | CMTEwith of module_type_ast * with_declaration_ast
+
+type module_ast = 
+  | CMEident of qualid located
+  | CMEapply of module_ast * module_ast
+
+(* Special identifier to encode recursive notations *)
+val ldots_var : identifier