diff options
| author | Maxime Dénès | 2017-12-18 09:38:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-18 09:38:18 +0100 |
| commit | 3da76841125ef48889c8eceb134116e2d0bd7a2e (patch) | |
| tree | 8728b456dab71560379044459e7a7c979a1b252b /plugins/funind/indfun.ml | |
| parent | 0168ee0b6463a9ef44d768b0020b34785986c1cb (diff) | |
| parent | 1172b52735a299dfc91aee36b30b576dfeff581c (diff) | |
Merge PR #6419: [vernac] Split `command.ml` into separate files.
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 357755e46f..071599d9c5 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -406,7 +406,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp match fixpoint_exprl with | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - Command.do_definition + ComDefinition.do_definition + ~program_mode:false fname (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); @@ -426,7 +427,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> @@ -616,8 +617,8 @@ and rebuild_nal aux bk bl' nal typ = let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = - let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in + let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in + let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = |