diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 4 | ||||
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 4 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 26 | ||||
| -rw-r--r-- | contrib/subtac/subtac_classes.ml | 4 |
4 files changed, 20 insertions, 18 deletions
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 62f1148320..67ae85d648 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -1370,7 +1370,7 @@ let do_build_inductive let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> (a , b, c , Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , None, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = @@ -1385,7 +1385,7 @@ let do_build_inductive let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> (a , b, c , Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , None, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = 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, diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index a240744bfc..510229ae6f 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -137,7 +137,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let sigma = Evd.evars_of !isevars in let subst = List.map (Evarutil.nf_evar sigma) subst in let subst = - let props = match props with CRecord (loc, _, fs) -> fs | _ -> assert false in + let props = match props with CRecord (loc, _, fs) -> fs + | _ -> errorlabstrm "new_instance" (Pp.str "Expected a record declaration for the instance body") + in if List.length props > List.length k.cl_props then Classes.mismatched_props env' (List.map snd props) k.cl_props; match k.cl_props with |