diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 4 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 26 |
2 files changed, 15 insertions, 15 deletions
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index f41d88bd60..d6ef1ea3b6 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -107,9 +107,9 @@ let convert_one_inductive sp tyi = let env = Global.env () in let envpar = push_rel_context params env in let sp = sp_of_global (IndRef (sp, tyi)) in - (((dummy_loc,basename sp), + (((false,(dummy_loc,basename sp)), convert_env(List.rev params), - Some (extern_constr true envpar arity), + Some (extern_constr true envpar arity), None, Constructors (convert_constructors envpar cstrnames cstrtypes)), None);; (* This function converts a Mutual inductive definition to a Coqast.t. diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index b404478ffb..6d6a0c0656 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1969,22 +1969,22 @@ let rec xlate_vernac = translated_restriction) | SearchAbout [] -> assert false) - | (*Record from tactics/Record.v *) - VernacRecord - (_, (add_coercion, (_,s)), binders, c1, - rec_constructor_or_none, field_list) -> - let record_constructor = - xlate_ident_opt (Option.map snd rec_constructor_or_none) in - CT_record - ((if add_coercion then CT_coercion_atm else - CT_coerce_NONE_to_COERCION_OPT(CT_none)), - xlate_ident s, xlate_binder_list binders, - xlate_formula (Option.get c1), record_constructor, - build_record_field_list field_list) +(* | (\*Record from tactics/Record.v *\) *) +(* VernacRecord *) +(* (_, (add_coercion, (_,s)), binders, c1, *) +(* rec_constructor_or_none, field_list) -> *) +(* let record_constructor = *) +(* xlate_ident_opt (Option.map snd rec_constructor_or_none) in *) +(* CT_record *) +(* ((if add_coercion then CT_coercion_atm else *) +(* CT_coerce_NONE_to_COERCION_OPT(CT_none)), *) +(* xlate_ident s, xlate_binder_list binders, *) +(* xlate_formula (Option.get c1), record_constructor, *) +(* build_record_field_list field_list) *) | VernacInductive (isind, lmi) -> let co_or_ind = if isind then "Inductive" else "CoInductive" in let strip_mutind = function - (((_,s), parameters, c, Constructors constructors), notopt) -> + (((_, (_,s)), parameters, c, _, Constructors constructors), notopt) -> CT_ind_spec (xlate_ident s, xlate_binder_list parameters, xlate_formula (Option.get c), build_constructors constructors, |