aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml996
-rw-r--r--interp/constrextern.mli7
-rw-r--r--interp/constrintern.ml38
-rw-r--r--interp/constrintern.mli5
-rw-r--r--interp/coqlib.ml84
-rw-r--r--interp/coqlib.mli18
-rw-r--r--interp/genarg.ml16
-rw-r--r--interp/genarg.mli9
-rw-r--r--interp/notation.ml4
-rw-r--r--interp/reserve.ml8
-rw-r--r--interp/topconstr.ml60
-rw-r--r--interp/topconstr.mli7
12 files changed, 94 insertions, 1158 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7c91eca25..5b448efef 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -69,13 +69,6 @@ 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 *)
@@ -96,8 +89,7 @@ let ids_of_ctxt ctxt =
(function c -> match kind_of_term c with
| Var id -> id
| _ ->
- error
- "Termast: arbitrary substitution of references not yet implemented")
+ error "arbitrary substitution of references not implemented")
ctxt)
let idopt_of_name = function
@@ -123,863 +115,8 @@ let raw_string_of_ref = function
| 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)
+ try Qualid (loc,shortest_qualid_of_global vars r)
with Not_found ->
(* happens in debugger *)
Ident (loc,id_of_string (raw_string_of_ref r))
@@ -1046,9 +183,6 @@ let rec check_same_type ty1 ty2 =
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 -> ()
@@ -1118,7 +252,7 @@ let rec same_raw c d =
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)}) ->
+ (fun (t1,(al1,oind1)) (t2,(al2,oind2)) ->
same_raw t1 t2;
if al1 <> al2 then failwith "RCases";
option_iter2(fun (_,i1,nl1) (_,i2,nl2) ->
@@ -1126,9 +260,6 @@ let rec same_raw c d =
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;
@@ -1213,33 +344,6 @@ let make_pat_notation loc ntn 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,Evd.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,Evd.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
@@ -1294,14 +398,14 @@ let rec extern_cases_pattern_in_scope scopes vars pat =
(Notation.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,Name id) -> CPatAtom (loc,Some (Ident (loc,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)
+ | Name id -> CPatAlias (loc,p,id)
| Anonymous -> p)
and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
@@ -1354,24 +458,6 @@ let is_projection nargs = function
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 =
@@ -1388,10 +474,12 @@ let explicitize loc inctx impl (cf,f) args =
!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))))
+ (not (is_inferable_implicit inctx n imp)))
in
- if visible then (a,Some (explicit_code imp q)) :: tail else tail
+ if visible then
+ (a,Some (dummy_loc, ExplByName (name_of_implicit imp))) :: 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
@@ -1511,10 +599,10 @@ let rec extern inctx scopes vars r =
extern_symbol scopes vars r (Notation.uninterp_notations r)
with No_match -> match r with
| RRef (loc,ref) ->
- extern_global loc (implicits_of_global_out ref)
+ extern_global loc (implicits_of_global ref)
(extern_reference loc vars ref)
- | RVar (loc,id) -> CRef (Ident (loc,v7_to_v8_id id))
+ | RVar (loc,id) -> CRef (Ident (loc,id))
| REvar (loc,n,_) -> (* we drop args *) extern_evar loc n
@@ -1526,14 +614,9 @@ let rec extern inctx scopes vars r =
let subscopes = Notation.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)
+ extern_app loc inctx (implicits_of_global 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))
@@ -1543,7 +626,6 @@ let rec extern inctx scopes vars r =
CArrow (loc,extern_typ scopes vars t, extern_typ 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)
@@ -1557,16 +639,15 @@ let rec extern inctx scopes vars r =
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_typ scopes vars) typopt in
+ | RCases (loc,rtntypopt,tml,eqns) ->
let vars' =
List.fold_right (name_fold Idset.add)
(cases_predicate_names tml) vars in
- let rtntypopt' = option_app (extern_typ scopes vars') !rtntypopt in
- let tml = List.map (fun (tm,{contents=(na,x)}) ->
+ let rtntypopt' = option_app (extern_typ scopes vars') rtntypopt in
+ let tml = List.map (fun (tm,(na,x)) ->
let na' = match na,tm with
Anonymous, RVar (_,id) when
- !rtntypopt<>None & occur_rawconstr id (out_some !rtntypopt)
+ rtntypopt<>None & occur_rawconstr id (out_some rtntypopt)
-> Some Anonymous
| Anonymous, _ -> None
| Name id, RVar (_,id') when id=id' -> None
@@ -1578,31 +659,8 @@ let rec extern inctx scopes vars r =
| Name id -> RVar (dummy_loc,id)) nal in
let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),args) in
(extern_typ 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_typ 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_typ scopes vars) typopt,
- sub_extern false scopes vars tm,Array.to_list bv)
+ let eqns = List.map (extern_eqn (rtntypopt<>None) scopes vars) eqns in
+ CCases (loc,rtntypopt',tml,eqns)
| RLetTuple (loc,nal,(na,typopt),tm,b) ->
CLetTuple (loc,nal,
@@ -1670,8 +728,7 @@ and factorize_prod scopes vars aty = function
| RProd (loc,(Name id as na),ty,c)
when same aty (extern_typ 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
+ -> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in
((loc,Name id)::nal,c)
| c -> ([],extern_typ scopes vars c)
@@ -1679,8 +736,7 @@ and factorize_lambda inctx scopes vars aty = function
| RLambda (loc,na,ty,c)
when same aty (extern_typ 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) =
+ -> 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)
@@ -1688,14 +744,12 @@ and factorize_lambda inctx scopes vars aty = function
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_typ 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)
@@ -1815,12 +869,10 @@ let rec raw_of_pat tenv env = function
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)],[])
+ if typopt <> None then failwith "TODO: PCase to RCases";
+ RCases (loc,(*(option_app (raw_of_pat tenv env) typopt,*)None,
+ [raw_of_pat tenv env tm,(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
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 059b13c57..e97d778c3 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -24,9 +24,6 @@ open Notation
(*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
@@ -72,7 +69,3 @@ 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
index 0795009b6..e81295214 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -42,10 +42,6 @@ let for_grammar f x =
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 *)
@@ -254,8 +250,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
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)
+ RVar (loc,id), impl, argsc, 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
@@ -318,13 +313,6 @@ 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))
@@ -665,8 +653,7 @@ let check_projection isproj nargs r =
| _, None -> ()
let get_implicit_name n imps =
- if !Options.v7 then None
- else Some (Impargs.name_of_implicit (List.nth imps (n-1)))
+ Some (Impargs.name_of_implicit (List.nth imps (n-1)))
let set_hole_implicit i = function
| RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i))
@@ -884,21 +871,15 @@ let internalise sigma env allow_soapp lvar c =
(* 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) ->
+ | CCases (loc, 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)
+ (tm,ind)::inds,List.fold_left (push_name_env lvar) env nal)
tms ([],env) in
let rtnpo = option_app (intern_type env') rtnpo in
let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
- RCases (loc, (option_app (intern_type env) po, ref rtnpo), tms,
- List.flatten 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)
+ RCases (loc, rtnpo, tms, List.flatten eqns')
| 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
@@ -916,13 +897,8 @@ let internalise sigma env allow_soapp lvar c =
RHole (loc, Evd.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)) ->
- if List.mem n (fst (let (a,_,_,_) = lvar in a)) & !Options.v7 then
- RVar (loc, n)
- else
- error_unbound_patvar loc n
+ error_unbound_patvar loc n
| CPatVar (loc, _) ->
raise (InternalisationError (loc,NegativeMetavariable))
| CEvar (loc, n) ->
@@ -986,7 +962,7 @@ let internalise sigma env allow_soapp lvar c =
| None ->
[], None in
let na = match tm', na with
- | RVar (_,id), None when Idset.mem id vars & not !Options.v7 -> Name id
+ | RVar (_,id), None when Idset.mem id vars -> Name id
| _, None -> Anonymous
| _, Some na -> na in
(tm',(na,typ)), na::ids
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 08de85d87..70af93885 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -17,7 +17,6 @@ open Environ
open Libnames
open Rawterm
open Pattern
-open Coqast
open Topconstr
open Termops
open Pretyping
@@ -116,7 +115,3 @@ val for_grammar : ('a -> 'b) -> 'a -> 'b
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
index 3a0a5047b..ba3b3d872 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -23,8 +23,7 @@ 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
+ let sp = Libnames.make_path dir (id_of_string s) in
try
Nametab.absolute_reference sp
with Not_found ->
@@ -46,7 +45,7 @@ let has_suffix_in_dirs dirs ref =
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 id = id_of_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
@@ -181,9 +180,10 @@ let build_coq_eq_data () = {
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 }
+ sym = Lazy.force coq_eq_sym }
let build_coq_eq () = Lazy.force coq_eq_eq
+let build_coq_sym_eq () = Lazy.force coq_eq_sym
let build_coq_f_equal2 () = Lazy.force coq_f_equal2
(* Specif *)
@@ -191,56 +191,23 @@ 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"
+let coq_identity_eq = lazy_init_constant ["Datatypes"] "identity"
+let coq_identity_refl = lazy_init_constant ["Datatypes"] "refl_identity"
+let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind"
+let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec"
+let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect"
+let coq_identity_congr = lazy_init_constant ["Logic_Type"] "congr_id"
+let coq_identity_sym = lazy_init_constant ["Logic_Type"] "sym_id"
+
+let build_coq_identity_data () = {
+ eq = Lazy.force coq_identity_eq;
+ refl = Lazy.force coq_identity_refl;
+ ind = Lazy.force coq_identity_ind;
+ rrec = Some (Lazy.force coq_identity_rec);
+ rect = Some (Lazy.force coq_identity_rect);
+ congr = Lazy.force coq_identity_congr;
+ sym = Lazy.force coq_identity_sym }
(* The False proposition *)
let coq_False = lazy_init_constant ["Logic"] "False"
@@ -256,10 +223,6 @@ 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
@@ -285,8 +248,8 @@ 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_identity_pattern =
+ lazy (snd (parse_pattern "(Coq.Init.Logic_Type.identity ?1 ?2 ?3)"))
let coq_existS_pattern =
lazy (snd (parse_pattern "(Coq.Init.Specif.existS ?1 ?2 ?3 ?4)"))
let coq_existT_pattern =
@@ -305,8 +268,7 @@ let coq_eqdec_pattern =
(* 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_identity_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")
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 64c83d7eb..f74190a0e 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -80,20 +80,11 @@ type coq_leibniz_eq_data = {
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_identity_data : coq_leibniz_eq_data delayed
-val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *)
+val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *)
+val build_coq_sym_eq : constr delayed (* = [(build_coq_eq_data()).sym] *)
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
@@ -119,8 +110,7 @@ val build_coq_or : constr delayed
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_identity_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
diff --git a/interp/genarg.ml b/interp/genarg.ml
index d9afc146b..1b2f48f95 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -26,13 +26,13 @@ type argument_type =
| PreIdentArgType
| IntroPatternArgType
| IdentArgType
- | HypArgType
+ | VarArgType
| RefArgType
(* Specific types *)
| SortArgType
| ConstrArgType
| ConstrMayEvalArgType
- | QuantHypArgType
+ | QuantVarArgType
| TacticArgType of int
| OpenConstrArgType of bool
| ConstrWithBindingsArgType
@@ -116,17 +116,17 @@ 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_var = VarArgType
+let globwit_var = VarArgType
+let wit_var = VarArgType
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_quant_hyp = QuantVarArgType
+let globwit_quant_hyp = QuantVarArgType
+let wit_quant_hyp = QuantVarArgType
let rawwit_sort = SortArgType
let globwit_sort = SortArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 9609576a4..50c8ab3e0 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -71,7 +71,7 @@ VarArgType identifier constr
RefArgType reference global_reference
ConstrArgType constr_expr constr
ConstrMayEvalArgType constr_expr may_eval constr
-QuantHypArgType quantified_hypothesis quantified_hypothesis
+QuantVarArgType quantified_hypothesis quantified_hypothesis
TacticArgType raw_tactic_expr tactic
OpenConstrArgType constr_expr open_constr
ConstrBindingsArgType constr_expr with_bindings constr with_bindings
@@ -114,7 +114,7 @@ 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 wit_var : (identifier,'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
@@ -231,13 +231,13 @@ type argument_type =
| PreIdentArgType
| IntroPatternArgType
| IdentArgType
- | HypArgType
+ | VarArgType
| RefArgType
(* Specific types *)
| SortArgType
| ConstrArgType
| ConstrMayEvalArgType
- | QuantHypArgType
+ | QuantVarArgType
| TacticArgType of int
| OpenConstrArgType of bool
| ConstrWithBindingsArgType
@@ -271,4 +271,3 @@ 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/notation.ml b/interp/notation.ml
index f116f292c..570981aff 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -31,7 +31,7 @@ open Ppextend
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])
+ this scope
- 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
@@ -261,7 +261,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
(* Uninterpreted notation levels *)
let declare_notation_level ntn level =
- if not !Options.v7 & Stringmap.mem ntn !notation_level_map then
+ if 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
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 917f9f4ad..834587f8d 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -57,14 +57,11 @@ let rec unloc = function
| 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 (_,rtntypopt,tml,pl) ->
RCases (dummy_loc,
- (option_app unloc tyopt,ref (option_app unloc !rtntypopt)),
+ (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) ->
@@ -86,7 +83,6 @@ let rec unloc = function
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,Evd.BinderType na)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index ae6bcd10c..c75cc8575 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -37,10 +37,9 @@ type aconstr =
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
- | ACases of aconstr option * aconstr option *
+ | ACases of 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
@@ -73,7 +72,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
let e,na = name_app g e na in RProd (loc,na,f e ty,f e c)
| ALetIn (na,b,c) ->
let e,na = name_app g e na in RLetIn (loc,na,f e b,f e c)
- | ACases (tyopt,rtntypopt,tml,eqnl) ->
+ | ACases (rtntypopt,tml,eqnl) ->
let cases_predicate_names tml =
List.flatten (List.map (function
| (tm,(na,None)) -> [na]
@@ -84,11 +83,9 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
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)),
+ RCases (loc,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)
+ (f e tm,(na,option_app (fun (x,y) -> (loc,x,y)) x))) tml,eqnl)
| ALetTuple (nal,(na,po),b,c) ->
let e,nal = list_fold_map (name_app g) e nal in
let e,na = name_app g e na in
@@ -129,9 +126,9 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
f ty1 ty2 & f c1 c2
| RHole _, RHole _ -> true
| RSort (_,s1), RSort (_,s2) -> s1 = s2
- | (RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _
+ | (RLetIn _ | RCases _ | RRec _ | RDynamic _
| RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
- | _,(RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _
+ | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
| RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
-> error "Unsupported construction in recursive notations"
| (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
@@ -175,20 +172,17 @@ let aconstr_and_vars_of_rawconstr a =
| RLambda (_,na,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
| RProd (_,na,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
| RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
- | RCases (_,(tyopt,rtntypopt),tml,eqnl) ->
+ | RCases (_,rtntypopt,tml,eqnl) ->
let f (_,idl,pat,rhs) =
found := idl@(!found);
(idl,pat,aux rhs) in
- ACases (option_app aux tyopt,
- option_app aux !rtntypopt,
- List.map (fun (tm,{contents = (na,x)}) ->
+ ACases (option_app aux rtntypopt,
+ List.map (fun (tm,(na,x)) ->
add_name found na;
option_iter
(fun (_,_,nl) -> List.iter (add_name found) 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) ->
add_name found na;
List.iter (add_name found) nal;
@@ -284,9 +278,8 @@ let rec subst_aconstr subst bound raw =
if r1' == r1 && r2' == r2 then raw else
ALetIn (n,r1',r2')
- | ACases (ro,rtntypopt,rl,branches) ->
- let ro' = option_smartmap (subst_aconstr subst bound) ro
- and rtntypopt' = option_smartmap (subst_aconstr subst bound) rtntypopt
+ | ACases (rtntypopt,rl,branches) ->
+ let rtntypopt' = option_smartmap (subst_aconstr subst bound) rtntypopt
and rl' = list_smartmap
(fun (a,(n,signopt) as x) ->
let a' = subst_aconstr subst bound a in
@@ -303,16 +296,9 @@ let rec subst_aconstr subst bound raw =
(idl,cpl',r'))
branches
in
- if ro' == ro && rtntypopt == rtntypopt' &
+ if rtntypopt' == rtntypopt && 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 bound) ro
- and r' = subst_aconstr subst bound r
- and ra' = array_smartmap (subst_aconstr subst bound) ra in
- if ro' == ro && r' == r && ra' == ra then raw else
- AOrderedCase (b,ro',r',ra')
+ ACases (rtntypopt',rl',branches')
| ALetTuple (nal,(na,po),b,c) ->
let po' = option_smartmap (subst_aconstr subst bound) po
@@ -402,17 +388,13 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
| RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) ->
match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
- | RCases (_,(po1,rtno1),tml1,eqnl1), ACases (po2,rtno2,tml2,eqnl2)
+ | RCases (_,rtno1,tml1,eqnl1), ACases (rtno2,tml2,eqnl2)
when List.length tml1 = List.length tml2 ->
- let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in
+ let sigma = option_fold_left2 (match_ alp metas) sigma rtno1 rtno2 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
| RIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) ->
let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
List.fold_left2 (match_ alp metas) sigma [a1;b1;c1] [a2;b2;c2]
@@ -507,11 +489,9 @@ type 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) *
+ | CCases of loc * 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)
@@ -562,7 +542,6 @@ let constr_loc = function
| CAppExpl (loc,_,_) -> loc
| CApp (loc,_,_) -> loc
| CCases (loc,_,_,_) -> loc
- | COrderedCase (loc,_,_,_,_) -> loc
| CLetTuple (loc,_,_,_,_) -> loc
| CIf (loc,_,_,_,_) -> loc
| CHole loc -> loc
@@ -605,7 +584,6 @@ let rec occur_var_constr_expr id = function
| 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,_,_)
@@ -676,7 +654,7 @@ let map_constr_expr_with_binders f g e = function
| 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) ->
+ | CCases (loc,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' =
@@ -689,10 +667,8 @@ let map_constr_expr_with_binders f g e = function
indnal (option_fold_right (name_fold g) na e))
a e
in
- CCases (loc,(option_app (f e) po, option_app (f e') rtnpo),
+ CCases (loc,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
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 0a073c435..e0f5ad577 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -33,10 +33,9 @@ type aconstr =
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
- | ACases of aconstr option * aconstr option *
+ | ACases of 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
@@ -91,11 +90,9 @@ type 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) *
+ | CCases of loc * 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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 15:59:15 +0000