adaptation V8 version Pierre Cregut

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5428 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 321 insertions, 106 deletions

diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 28a969bab..b89661431 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -7,7 +7,7 @@
  *************************************************************************)
 
 let module_refl_name = "ReflOmegaCore"
-let module_refl_path = ["romega"; module_refl_name]
+let module_refl_path = ["Coq"; "romega"; module_refl_name]
 
 type result = 
    Kvar of string
@@ -17,19 +17,20 @@ type result =
 
 let destructurate t =
   let c, args = Term.decompose_app t in
-(*  let env = Global.env() in*)
+  let env = Global.env() in
   match Term.kind_of_term c, args with
     | Term.Const sp, args ->
 	Kapp (Names.string_of_id
 		(Nametab.id_of_global (Libnames.ConstRef sp)),
-              args)
+	      args)
     | Term.Construct csp , args ->
 	Kapp (Names.string_of_id
 		(Nametab.id_of_global (Libnames.ConstructRef csp)),
-	        args)
+	      args)
     | Term.Ind isp, args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global (Libnames.IndRef isp)),args)
+		(Nametab.id_of_global (Libnames.IndRef isp)),
+	      args)
     | Term.Var id,[] -> Kvar(Names.string_of_id id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
     | Term.Prod (Names.Name _,_,_),[] ->
@@ -39,15 +40,14 @@ let destructurate t =
 exception Destruct
 
 let dest_const_apply t = 
-  let f,args = Term.decompose_app t in
+  let f,args = Term.decompose_app t in 
   let ref = 
   match Term.kind_of_term f with 
     | Term.Const sp         -> Libnames.ConstRef sp
     | Term.Construct csp -> Libnames.ConstructRef csp
     | Term.Ind isp       -> Libnames.IndRef isp
     | _ -> raise Destruct
-  in
-  Nametab.id_of_global ref, args
+  in  Nametab.id_of_global ref, args
 
 let recognize_number t =
   let rec loop t =
@@ -62,26 +62,17 @@ let recognize_number t =
        "POS",[t] -> loop t | "NEG",[t] -> - (loop t) | "ZERO",[] -> 0
      | _ -> failwith "not a number";;
 
-let init_dir = ["Coq";"Init"]
-let arith_dir = ["Coq";"Arith"]
-let logic_dir = ["Coq";"Logic"]
-let zarith_dir = ["Coq";"ZArith"]
-let list_dir = ["Coq";"Lists"]
-let coq_modules = [
-  zarith_dir@["fast_integer"];
-  zarith_dir@["zarith_aux"];
-  zarith_dir@["auxiliary"];
-  init_dir@["Datatypes"];
-  init_dir@["Peano"];
-  init_dir@["Logic"];
-  arith_dir@["Compare_dec"];
-  arith_dir@["Peano_dec"];
-  arith_dir@["Minus"];
-  logic_dir@["Decidable"];
-  list_dir@["PolyList"]
-]
-
-let constant = Coqlib.gen_constant_in_modules "ROmega" coq_modules
+
+let logic_dir = ["Coq";"Logic";"Decidable"]
+
+let coq_modules =
+  Coqlib.init_modules @ [logic_dir] @ Coqlib.arith_modules @ Coqlib.zarith_base_modules
+    @ [["Coq"; "omega"; "OmegaLemmas"]]
+    @ [["Coq"; "Lists"; (if !Options.v7 then "PolyList" else "List")]]
+    @ [module_refl_path]
+
+
+let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules
 
 let coq_xH = lazy (constant "xH")
 let coq_xO = lazy (constant "xO")
@@ -90,119 +81,334 @@ let coq_ZERO = lazy (constant "ZERO")
 let coq_POS = lazy (constant "POS")
 let coq_NEG = lazy (constant "NEG")
 let coq_Z = lazy (constant "Z")
-let coq_relation = lazy (constant "relation")
+let coq_relation = lazy (constant  (if !Options.v7 then "relation" else "comparis
+on"))
 let coq_SUPERIEUR = lazy (constant "SUPERIEUR")
 let coq_INFEEIEUR = lazy (constant "INFERIEUR")
 let coq_EGAL = lazy (constant "EGAL")
 let coq_Zplus = lazy (constant "Zplus")
-let coq_Zmult = lazy (constant "Zmult")
+let coq_Zmult = lazy (constant  "Zmult")
 let coq_Zopp = lazy (constant "Zopp")
 
-(* auxiliaires zarith *)
 let coq_Zminus = lazy (constant "Zminus")
-let coq_Zs = lazy (constant "Zs")
+let coq_Zs = lazy (constant  "Zs")
 let coq_Zgt = lazy (constant "Zgt")
 let coq_Zle = lazy (constant "Zle")
-let coq_inject_nat = lazy (constant "inject_nat")
+let coq_inject_nat = lazy (constant  "inject_nat")
 
 (* Peano *)
 let coq_le = lazy(constant "le")
 let coq_gt = lazy(constant "gt")
 
-(* Datatypes *)
+(* Integers *)
 let coq_nat = lazy(constant "nat")
 let coq_S = lazy(constant "S")
 let coq_O = lazy(constant "O")
-
-(* Minus *)
 let coq_minus = lazy(constant "minus")
 
 (* Logic *)
-let coq_eq = lazy(constant "eq")
-let coq_refl_equal = lazy(constant "refl_equal")
+let coq_eq = lazy(constant  "eq")
+let coq_refl_equal = lazy(constant  "refl_equal")
 let coq_and = lazy(constant "and")
 let coq_not = lazy(constant "not")
 let coq_or = lazy(constant "or")
+let coq_true = lazy(constant "true")
+let coq_false = lazy(constant "false")
 let coq_ex = lazy(constant "ex")
+let coq_I = lazy(constant "I")
 
 (* Lists *)
 let coq_cons =  lazy (constant "cons")
 let coq_nil =  lazy (constant "nil")
 
-let romega_constant = Coqlib.gen_constant "ROmega" module_refl_path
-
-let coq_t_nat = lazy (romega_constant "Tint")
-let coq_t_plus = lazy (romega_constant "Tplus")
-let coq_t_mult = lazy (romega_constant "Tmult")
-let coq_t_opp = lazy (romega_constant "Topp")
-let coq_t_minus = lazy (romega_constant "Tminus")
-let coq_t_var = lazy (romega_constant "Tvar")
-let coq_t_equal = lazy (romega_constant "EqTerm")
-let coq_t_leq = lazy (romega_constant "LeqTerm")
-let coq_t_geq = lazy (romega_constant "GeqTerm")
-let coq_t_lt = lazy (romega_constant "LtTerm")
-let coq_t_gt = lazy (romega_constant "GtTerm")
-let coq_t_neq = lazy (romega_constant "NeqTerm")
-
-let coq_proposition = lazy (romega_constant "proposition")
-let coq_interp_sequent = lazy (romega_constant "interp_goal")
-let coq_normalize_sequent = lazy (romega_constant "normalize_goal")
-let coq_execute_sequent = lazy (romega_constant "execute_goal")
-let coq_sequent_to_hyps = lazy (romega_constant "goal_to_hyps")
+let coq_pcons = lazy (constant "Pcons")
+let coq_pnil = lazy (constant "Pnil")
+
+let coq_h_step = lazy (constant "h_step")
+let coq_pair_step = lazy (constant  "pair_step")
+let coq_p_left = lazy (constant  "P_LEFT")
+let coq_p_right = lazy (constant  "P_RIGHT")
+let coq_p_invert = lazy (constant  "P_INVERT")
+let coq_p_step = lazy (constant  "P_STEP")
+let coq_p_nop = lazy (constant  "P_NOP")
+
+
+let coq_t_int = lazy (constant  "Tint")
+let coq_t_plus = lazy (constant  "Tplus")
+let coq_t_mult = lazy (constant  "Tmult")
+let coq_t_opp = lazy (constant  "Topp")
+let coq_t_minus = lazy (constant  "Tminus")
+let coq_t_var = lazy (constant  "Tvar")
+
+let coq_p_eq = lazy (constant  "EqTerm")
+let coq_p_leq = lazy (constant  "LeqTerm")
+let coq_p_geq = lazy (constant  "GeqTerm")
+let coq_p_lt = lazy (constant  "LtTerm")
+let coq_p_gt = lazy (constant  "GtTerm")
+let coq_p_neq = lazy (constant  "NeqTerm")
+let coq_p_true = lazy (constant  "TrueTerm")
+let coq_p_false = lazy (constant  "FalseTerm")
+let coq_p_not = lazy (constant  "Tnot")
+let coq_p_or = lazy (constant  "Tor")
+let coq_p_and = lazy (constant  "Tand")
+let coq_p_imp = lazy (constant  "Timp")
+let coq_p_prop = lazy (constant  "Tprop")
+
+let coq_proposition = lazy (constant  "proposition")
+let coq_interp_sequent = lazy (constant  "interp_goal_concl")
+let coq_normalize_sequent = lazy (constant  "normalize_goal")
+let coq_execute_sequent = lazy (constant  "execute_goal")
+let coq_do_concl_to_hyp =  lazy (constant  "do_concl_to_hyp")
+let coq_sequent_to_hyps = lazy (constant  "goal_to_hyps")
+let coq_normalize_hyps_goal =
+  lazy (constant  "normalize_hyps_goal")
 
 (* Constructors for shuffle tactic *)
-let coq_t_fusion =  lazy (romega_constant "t_fusion")
-let coq_f_equal =  lazy (romega_constant "F_equal")
-let coq_f_cancel =  lazy (romega_constant "F_cancel")
-let coq_f_left =  lazy (romega_constant "F_left")
-let coq_f_right =  lazy (romega_constant "F_right")
+let coq_t_fusion =  lazy (constant  "t_fusion")
+let coq_f_equal =  lazy (constant  "F_equal")
+let coq_f_cancel =  lazy (constant  "F_cancel")
+let coq_f_left =  lazy (constant  "F_left")
+let coq_f_right =  lazy (constant  "F_right")
 
 (* Constructors for reordering tactics *)
-let coq_step = lazy (romega_constant "step")
-let coq_c_do_both = lazy (romega_constant "C_DO_BOTH")
-let coq_c_do_left = lazy (romega_constant "C_LEFT")
-let coq_c_do_right = lazy (romega_constant "C_RIGHT")
-let coq_c_do_seq = lazy (romega_constant "C_SEQ")
-let coq_c_nop = lazy (romega_constant "C_NOP")
-let coq_c_opp_plus = lazy (romega_constant "C_OPP_PLUS")
-let coq_c_opp_opp = lazy (romega_constant "C_OPP_OPP")
-let coq_c_opp_mult_r = lazy (romega_constant "C_OPP_MULT_R")
-let coq_c_opp_one = lazy (romega_constant "C_OPP_ONE")
-let coq_c_reduce = lazy (romega_constant "C_REDUCE")
-let coq_c_mult_plus_distr = lazy (romega_constant "C_MULT_PLUS_DISTR")
-let coq_c_opp_left = lazy (romega_constant "C_MULT_OPP_LEFT")
-let coq_c_mult_assoc_r = lazy (romega_constant "C_MULT_ASSOC_R")
-let coq_c_plus_assoc_r = lazy (romega_constant "C_PLUS_ASSOC_R")
-let coq_c_plus_assoc_l = lazy (romega_constant "C_PLUS_ASSOC_L")
-let coq_c_plus_permute = lazy (romega_constant "C_PLUS_PERMUTE")
-let coq_c_plus_sym = lazy (romega_constant "C_PLUS_SYM")
-let coq_c_red0 = lazy (romega_constant "C_RED0")
-let coq_c_red1 = lazy (romega_constant "C_RED1")
-let coq_c_red2 = lazy (romega_constant "C_RED2")
-let coq_c_red3 = lazy (romega_constant "C_RED3")
-let coq_c_red4 = lazy (romega_constant "C_RED4")
-let coq_c_red5 = lazy (romega_constant "C_RED5")
-let coq_c_red6 = lazy (romega_constant "C_RED6")
-let coq_c_mult_opp_left = lazy (romega_constant "C_MULT_OPP_LEFT")
+let coq_step = lazy (constant  "step")
+let coq_c_do_both = lazy (constant  "C_DO_BOTH")
+let coq_c_do_left = lazy (constant  "C_LEFT")
+let coq_c_do_right = lazy (constant  "C_RIGHT")
+let coq_c_do_seq = lazy (constant  "C_SEQ")
+let coq_c_nop = lazy (constant  "C_NOP")
+let coq_c_opp_plus = lazy (constant  "C_OPP_PLUS")
+let coq_c_opp_opp = lazy (constant  "C_OPP_OPP")
+let coq_c_opp_mult_r = lazy (constant  "C_OPP_MULT_R")
+let coq_c_opp_one = lazy (constant  "C_OPP_ONE")
+let coq_c_reduce = lazy (constant  "C_REDUCE")
+let coq_c_mult_plus_distr = lazy (constant  "C_MULT_PLUS_DISTR")
+let coq_c_opp_left = lazy (constant  "C_MULT_OPP_LEFT")
+let coq_c_mult_assoc_r = lazy (constant  "C_MULT_ASSOC_R")
+let coq_c_plus_assoc_r = lazy (constant  "C_PLUS_ASSOC_R")
+let coq_c_plus_assoc_l = lazy (constant  "C_PLUS_ASSOC_L")
+let coq_c_plus_permute = lazy (constant  "C_PLUS_PERMUTE")
+let coq_c_plus_sym = lazy (constant  "C_PLUS_SYM")
+let coq_c_red0 = lazy (constant  "C_RED0")
+let coq_c_red1 = lazy (constant  "C_RED1")
+let coq_c_red2 = lazy (constant  "C_RED2")
+let coq_c_red3 = lazy (constant  "C_RED3")
+let coq_c_red4 = lazy (constant  "C_RED4")
+let coq_c_red5 = lazy (constant  "C_RED5")
+let coq_c_red6 = lazy (constant  "C_RED6")
+let coq_c_mult_opp_left = lazy (constant  "C_MULT_OPP_LEFT")
 let coq_c_mult_assoc_reduced = 
-  lazy (romega_constant "C_MULT_ASSOC_REDUCED")
-let coq_c_minus = lazy (romega_constant "C_MINUS")
-let coq_c_mult_sym = lazy (romega_constant "C_MULT_SYM")
-
-let coq_s_constant_not_nul = lazy (romega_constant "O_CONSTANT_NOT_NUL")
-let coq_s_constant_neg = lazy (romega_constant "O_CONSTANT_NEG")
-let coq_s_div_approx = lazy (romega_constant "O_DIV_APPROX")
-let coq_s_not_exact_divide = lazy (romega_constant "O_NOT_EXACT_DIVIDE")
-let coq_s_exact_divide = lazy (romega_constant "O_EXACT_DIVIDE")
-let coq_s_sum = lazy (romega_constant "O_SUM")
-let coq_s_state = lazy (romega_constant "O_STATE")
-let coq_s_contradiction = lazy (romega_constant "O_CONTRADICTION")
-let coq_s_merge_eq = lazy (romega_constant "O_MERGE_EQ")
-let coq_s_split_ineq =lazy (romega_constant "O_SPLIT_INEQ")
-let coq_s_constant_nul =lazy (romega_constant "O_CONSTANT_NUL")
-let coq_s_negate_contradict =lazy (romega_constant "O_NEGATE_CONTRADICT")
-let coq_s_negate_contradict_inv =lazy (romega_constant "O_NEGATE_CONTRADICT_INV")
+  lazy (constant  "C_MULT_ASSOC_REDUCED")
+let coq_c_minus = lazy (constant  "C_MINUS")
+let coq_c_mult_sym = lazy (constant  "C_MULT_SYM")
+
+let coq_s_constant_not_nul = lazy (constant  "O_CONSTANT_NOT_NUL")
+let coq_s_constant_neg = lazy (constant  "O_CONSTANT_NEG")
+let coq_s_div_approx = lazy (constant  "O_DIV_APPROX")
+let coq_s_not_exact_divide = lazy (constant  "O_NOT_EXACT_DIVIDE")
+let coq_s_exact_divide = lazy (constant  "O_EXACT_DIVIDE")
+let coq_s_sum = lazy (constant  "O_SUM")
+let coq_s_state = lazy (constant  "O_STATE")
+let coq_s_contradiction = lazy (constant  "O_CONTRADICTION")
+let coq_s_merge_eq = lazy (constant  "O_MERGE_EQ")
+let coq_s_split_ineq =lazy (constant  "O_SPLIT_INEQ")
+let coq_s_constant_nul =lazy (constant  "O_CONSTANT_NUL")
+let coq_s_negate_contradict =lazy (constant  "O_NEGATE_CONTRADICT")
+let coq_s_negate_contradict_inv =lazy (constant  "O_NEGATE_CONTRADICT_INV")
+
+(* construction for the [extract_hyp] tactic *)
+let coq_direction = lazy  (constant  "direction")
+let coq_d_left = lazy  (constant  "D_left")
+let coq_d_right = lazy  (constant  "D_right")
+let coq_d_mono = lazy  (constant  "D_mono")
+
+let coq_e_split = lazy  (constant  "E_SPLIT")
+let coq_e_extract = lazy  (constant  "E_EXTRACT")
+let coq_e_solve = lazy  (constant  "E_SOLVE")
+
+let coq_decompose_solve_valid = 
+  lazy (constant   "decompose_solve_valid")
+let coq_do_reduce_lhyps = lazy (constant   "do_reduce_lhyps")
+let coq_do_omega = lazy (constant  "do_omega")
+
+(**
+let constant dir s =
+   try
+     Libnames.constr_of_reference 
+       (Nametab.absolute_reference
+	  (Libnames.make_path
+             (Names.make_dirpath (List.map Names.id_of_string (List.rev dir)))
+             (Names.id_of_string s)))
+   with e -> print_endline (String.concat "." dir); print_endline s;
+             raise e
+
+let path_fast_integer = ["Coq"; "ZArith"; "fast_integer"]
+let path_zarith_aux = ["Coq"; "ZArith"; "zarith_aux"]
+let path_logic = ["Coq"; "Init";"Logic"]
+let path_datatypes = ["Coq"; "Init";"Datatypes"]
+let path_peano = ["Coq"; "Init"; "Peano"]
+let path_list = ["Coq"; "Lists"; "PolyList"]
+
+let coq_xH = lazy (constant path_fast_integer "xH")
+let coq_xO = lazy (constant path_fast_integer "xO")
+let coq_xI = lazy (constant path_fast_integer "xI")
+let coq_ZERO = lazy (constant path_fast_integer "ZERO")
+let coq_POS = lazy (constant path_fast_integer "POS")
+let coq_NEG = lazy (constant path_fast_integer "NEG")
+let coq_Z = lazy (constant path_fast_integer "Z")
+let coq_relation = lazy (constant path_fast_integer "relation")
+let coq_SUPERIEUR = lazy (constant path_fast_integer "SUPERIEUR")
+let coq_INFEEIEUR = lazy (constant path_fast_integer "INFERIEUR")
+let coq_EGAL = lazy (constant path_fast_integer "EGAL")
+let coq_Zplus = lazy (constant path_fast_integer "Zplus")
+let coq_Zmult = lazy (constant path_fast_integer "Zmult")
+let coq_Zopp = lazy (constant path_fast_integer "Zopp")
+
+(* auxiliaires zarith *)
+let coq_Zminus = lazy (constant path_zarith_aux "Zminus")
+let coq_Zs = lazy (constant path_zarith_aux "Zs")
+let coq_Zgt = lazy (constant path_zarith_aux "Zgt")
+let coq_Zle = lazy (constant path_zarith_aux "Zle")
+let coq_inject_nat = lazy (constant path_zarith_aux "inject_nat")
+
+(* Peano *)
+let coq_le = lazy(constant path_peano "le")
+let coq_gt = lazy(constant path_peano "gt")
+
+(* Integers *)
+let coq_nat = lazy(constant path_datatypes "nat")
+let coq_S = lazy(constant path_datatypes "S")
+let coq_O = lazy(constant path_datatypes "O")
+
+(* Minus *)
+let coq_minus = lazy(constant ["Arith"; "Minus"] "minus")
 
+(* Logic *)
+let coq_eq = lazy(constant path_logic "eq")
+let coq_refl_equal = lazy(constant path_logic "refl_equal")
+let coq_and = lazy(constant path_logic "and")
+let coq_not = lazy(constant path_logic "not")
+let coq_or = lazy(constant path_logic "or")
+let coq_true = lazy(constant path_logic "true")
+let coq_false = lazy(constant path_logic "false")
+let coq_ex = lazy(constant path_logic "ex")
+let coq_I = lazy(constant path_logic "I")
+
+(* Lists *)
+let coq_cons =  lazy (constant path_list  "cons")
+let coq_nil =  lazy (constant path_list "nil")
+
+let coq_pcons = lazy (constant module_refl_path "Pcons")
+let coq_pnil = lazy (constant module_refl_path "Pnil")
+
+let coq_h_step = lazy (constant module_refl_path "h_step")
+let coq_pair_step = lazy (constant module_refl_path "pair_step")
+let coq_p_left = lazy (constant module_refl_path "P_LEFT")
+let coq_p_right = lazy (constant module_refl_path "P_RIGHT")
+let coq_p_invert = lazy (constant module_refl_path "P_INVERT")
+let coq_p_step = lazy (constant module_refl_path "P_STEP")
+let coq_p_nop = lazy (constant module_refl_path "P_NOP")
+
+
+let coq_t_int = lazy (constant module_refl_path "Tint")
+let coq_t_plus = lazy (constant module_refl_path "Tplus")
+let coq_t_mult = lazy (constant module_refl_path "Tmult")
+let coq_t_opp = lazy (constant module_refl_path "Topp")
+let coq_t_minus = lazy (constant module_refl_path "Tminus")
+let coq_t_var = lazy (constant module_refl_path "Tvar")
+
+let coq_p_eq = lazy (constant module_refl_path "EqTerm")
+let coq_p_leq = lazy (constant module_refl_path "LeqTerm")
+let coq_p_geq = lazy (constant module_refl_path "GeqTerm")
+let coq_p_lt = lazy (constant module_refl_path "LtTerm")
+let coq_p_gt = lazy (constant module_refl_path "GtTerm")
+let coq_p_neq = lazy (constant module_refl_path "NeqTerm")
+let coq_p_true = lazy (constant module_refl_path "TrueTerm")
+let coq_p_false = lazy (constant module_refl_path "FalseTerm")
+let coq_p_not = lazy (constant module_refl_path "Tnot")
+let coq_p_or = lazy (constant module_refl_path "Tor")
+let coq_p_and = lazy (constant module_refl_path "Tand")
+let coq_p_imp = lazy (constant module_refl_path "Timp")
+let coq_p_prop = lazy (constant module_refl_path "Tprop")
+
+let coq_proposition = lazy (constant module_refl_path "proposition")
+let coq_interp_sequent = lazy (constant module_refl_path "interp_goal_concl")
+let coq_normalize_sequent = lazy (constant module_refl_path "normalize_goal")
+let coq_execute_sequent = lazy (constant module_refl_path "execute_goal")
+let coq_do_concl_to_hyp =  lazy (constant module_refl_path "do_concl_to_hyp")
+let coq_sequent_to_hyps = lazy (constant module_refl_path "goal_to_hyps")
+let coq_normalize_hyps_goal =
+  lazy (constant module_refl_path "normalize_hyps_goal")
+
+(* Constructors for shuffle tactic *)
+let coq_t_fusion =  lazy (constant module_refl_path "t_fusion")
+let coq_f_equal =  lazy (constant module_refl_path "F_equal")
+let coq_f_cancel =  lazy (constant module_refl_path "F_cancel")
+let coq_f_left =  lazy (constant module_refl_path "F_left")
+let coq_f_right =  lazy (constant module_refl_path "F_right")
+
+(* Constructors for reordering tactics *)
+let coq_step = lazy (constant module_refl_path "step")
+let coq_c_do_both = lazy (constant module_refl_path "C_DO_BOTH")
+let coq_c_do_left = lazy (constant module_refl_path "C_LEFT")
+let coq_c_do_right = lazy (constant module_refl_path "C_RIGHT")
+let coq_c_do_seq = lazy (constant module_refl_path "C_SEQ")
+let coq_c_nop = lazy (constant module_refl_path "C_NOP")
+let coq_c_opp_plus = lazy (constant module_refl_path "C_OPP_PLUS")
+let coq_c_opp_opp = lazy (constant module_refl_path "C_OPP_OPP")
+let coq_c_opp_mult_r = lazy (constant module_refl_path "C_OPP_MULT_R")
+let coq_c_opp_one = lazy (constant module_refl_path "C_OPP_ONE")
+let coq_c_reduce = lazy (constant module_refl_path "C_REDUCE")
+let coq_c_mult_plus_distr = lazy (constant module_refl_path "C_MULT_PLUS_DISTR")
+let coq_c_opp_left = lazy (constant module_refl_path "C_MULT_OPP_LEFT")
+let coq_c_mult_assoc_r = lazy (constant module_refl_path "C_MULT_ASSOC_R")
+let coq_c_plus_assoc_r = lazy (constant module_refl_path "C_PLUS_ASSOC_R")
+let coq_c_plus_assoc_l = lazy (constant module_refl_path "C_PLUS_ASSOC_L")
+let coq_c_plus_permute = lazy (constant module_refl_path "C_PLUS_PERMUTE")
+let coq_c_plus_sym = lazy (constant module_refl_path "C_PLUS_SYM")
+let coq_c_red0 = lazy (constant module_refl_path "C_RED0")
+let coq_c_red1 = lazy (constant module_refl_path "C_RED1")
+let coq_c_red2 = lazy (constant module_refl_path "C_RED2")
+let coq_c_red3 = lazy (constant module_refl_path "C_RED3")
+let coq_c_red4 = lazy (constant module_refl_path "C_RED4")
+let coq_c_red5 = lazy (constant module_refl_path "C_RED5")
+let coq_c_red6 = lazy (constant module_refl_path "C_RED6")
+let coq_c_mult_opp_left = lazy (constant module_refl_path "C_MULT_OPP_LEFT")
+let coq_c_mult_assoc_reduced = 
+  lazy (constant module_refl_path "C_MULT_ASSOC_REDUCED")
+let coq_c_minus = lazy (constant module_refl_path "C_MINUS")
+let coq_c_mult_sym = lazy (constant module_refl_path "C_MULT_SYM")
+
+let coq_s_constant_not_nul = lazy (constant module_refl_path "O_CONSTANT_NOT_NUL")
+let coq_s_constant_neg = lazy (constant module_refl_path "O_CONSTANT_NEG")
+let coq_s_div_approx = lazy (constant module_refl_path "O_DIV_APPROX")
+let coq_s_not_exact_divide = lazy (constant module_refl_path "O_NOT_EXACT_DIVIDE")
+let coq_s_exact_divide = lazy (constant module_refl_path "O_EXACT_DIVIDE")
+let coq_s_sum = lazy (constant module_refl_path "O_SUM")
+let coq_s_state = lazy (constant module_refl_path "O_STATE")
+let coq_s_contradiction = lazy (constant module_refl_path "O_CONTRADICTION")
+let coq_s_merge_eq = lazy (constant module_refl_path "O_MERGE_EQ")
+let coq_s_split_ineq =lazy (constant module_refl_path "O_SPLIT_INEQ")
+let coq_s_constant_nul =lazy (constant module_refl_path "O_CONSTANT_NUL")
+let coq_s_negate_contradict =lazy (constant module_refl_path "O_NEGATE_CONTRADICT")
+let coq_s_negate_contradict_inv =lazy (constant module_refl_path "O_NEGATE_CONTRADICT_INV")
+
+(* construction for the [extract_hyp] tactic *)
+let coq_direction = lazy  (constant module_refl_path "direction")
+let coq_d_left = lazy  (constant module_refl_path "D_left")
+let coq_d_right = lazy  (constant module_refl_path "D_right")
+let coq_d_mono = lazy  (constant module_refl_path "D_mono")
+
+let coq_e_split = lazy  (constant module_refl_path "E_SPLIT")
+let coq_e_extract = lazy  (constant module_refl_path "E_EXTRACT")
+let coq_e_solve = lazy  (constant module_refl_path "E_SOLVE")
+
+let coq_decompose_solve_valid = 
+  lazy (constant  module_refl_path "decompose_solve_valid")
+let coq_do_reduce_lhyps = lazy (constant  module_refl_path "do_reduce_lhyps")
+let coq_do_omega = lazy (constant module_refl_path "do_omega")
+
+*)
 (* \subsection{Construction d'expressions} *)
 
 
@@ -270,5 +476,14 @@ let mk_list typ l =
 	Term.mkApp (Lazy.force coq_cons, [|typ; step; loop l |]) in
   loop l
 
+let mk_plist l =
+  let rec loop = function
+    | [] ->
+	(Lazy.force coq_pnil)
+    | (step :: l) -> 
+	Term.mkApp (Lazy.force coq_pcons, [| step; loop l |]) in
+  loop l
+
+
 let mk_shuffle_list l = mk_list (Lazy.force coq_t_fusion) l