diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/command.ml | 21 | ||||
-rw-r--r-- | toplevel/command.mli | 4 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 7 |
3 files changed, 16 insertions, 16 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 720df5a80..24d292d49 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -381,10 +381,10 @@ let eq_local_binders bl1 bl2 = let extract_coercions indl = let mkqid (_,((_,id),_)) = make_short_qualid id in let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in - List.map mkqid (List.flatten(List.map (fun (_,_,_,_,lc) -> extract lc) indl)) + List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl)) let extract_params indl = - let paramsl = List.map (fun (_,_,params,_,_) -> params) indl in + let paramsl = List.map (fun (_,params,_,_) -> params) indl in match paramsl with | [] -> anomaly "empty list of inductive types" | params::paramsl -> @@ -392,13 +392,13 @@ let extract_params indl = "Parameters should be syntactically the same for each inductive type"; params -let prepare_inductive indl = - let ntnl,indl = - List.split (List.map (fun ((_,indname),ntn,_,ar,lc) -> ntn, { +let prepare_inductive ntnl indl = + let indl = + List.map (fun ((_,indname),_,ar,lc) -> { ind_name = indname; ind_arity = ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc - }) indl) in + }) indl in List.fold_right option_cons ntnl [], indl let declare_mutual_with_eliminations isrecord mie = @@ -408,10 +408,11 @@ let declare_mutual_with_eliminations isrecord mie = declare_eliminations kn; kn -let build_mutual indl finite = +let build_mutual l finite = + let indl,ntnl = List.split l in let paramsl = extract_params indl in let coes = extract_coercions indl in - let notations,indl = prepare_inductive indl in + let notations,indl = prepare_inductive ntnl indl in let mie = interp_mutual paramsl indl notations finite in (* Declare the mutual inductive block with its eliminations *) ignore (declare_mutual_with_eliminations false mie); @@ -604,8 +605,8 @@ let build_recursive l b = interp_recursive (IsFixpoint g) fixl b let build_corecursive l b = - let fixl = List.map (fun (id,bl,typ,def) -> - ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},None)) + let fixl = List.map (fun ((id,bl,typ,def),ntn) -> + ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn)) l in interp_recursive IsCoFixpoint fixl b diff --git a/toplevel/command.mli b/toplevel/command.mli index be589da1a..7c3d51946 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -39,14 +39,14 @@ val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit val declare_assumption : identifier located list -> coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit -val build_mutual : inductive_expr list -> bool -> unit +val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit val declare_mutual_with_eliminations : bool -> Entries.mutual_inductive_entry -> mutual_inductive val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit -val build_corecursive : cofixpoint_expr list -> bool -> unit +val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit val build_scheme : (identifier located * bool * reference * rawsort) list -> unit diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 51010afa8..8b654e12d 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -146,8 +146,7 @@ type simple_binder = lident list * constr_expr type 'a with_coercion = coercion_flag * 'a type constructor_expr = (lident * constr_expr) with_coercion type inductive_expr = - lident * decl_notation * local_binder list * constr_expr - * constructor_expr list + lident * local_binder list * constr_expr * constructor_expr list type definition_expr = | ProveBody of local_binder list * constr_expr | DefineBody of local_binder list * raw_red_expr option * constr_expr @@ -195,9 +194,9 @@ type vernac_expr = | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of assumption_kind * simple_binder with_coercion list - | VernacInductive of inductive_flag * inductive_expr list + | VernacInductive of inductive_flag * (inductive_expr * decl_notation) list | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool - | VernacCoFixpoint of cofixpoint_expr list * bool + | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool | VernacScheme of (lident * bool * lreference * sort_expr) list (* Gallina extensions *) |