diff options
| -rw-r--r-- | interp/interp.mllib | 1 | ||||
| -rw-r--r-- | tactics/declare.ml (renamed from interp/declare.ml) | 40 | ||||
| -rw-r--r-- | tactics/declare.mli (renamed from interp/declare.mli) | 4 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 1 |
4 files changed, 23 insertions, 23 deletions
diff --git a/interp/interp.mllib b/interp/interp.mllib index 52978a2ab6..33573edcce 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -17,4 +17,3 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Declare diff --git a/interp/declare.ml b/tactics/declare.ml index 77313a54de..a5b3c6cb45 100644 --- a/interp/declare.ml +++ b/tactics/declare.ml @@ -303,18 +303,18 @@ let inductive_names sp kn mie = let names, _ = List.fold_left (fun (names, n) ind -> - let ind_p = (kn,n) in - let names, _ = - List.fold_left - (fun (names, p) l -> - let sp = - Libnames.make_path dp l - in - ((sp, ConstructRef (ind_p,p)) :: names, p+1)) - (names, 1) ind.mind_entry_consnames in - let sp = Libnames.make_path dp ind.mind_entry_typename - in - ((sp, IndRef ind_p) :: names, n+1)) + let ind_p = (kn,n) in + let names, _ = + List.fold_left + (fun (names, p) l -> + let sp = + Libnames.make_path dp l + in + ((sp, ConstructRef (ind_p,p)) :: names, p+1)) + (names, 1) ind.mind_entry_consnames in + let sp = Libnames.make_path dp ind.mind_entry_typename + in + ((sp, IndRef ind_p) :: names, n+1)) ([], 0) mie.mind_entry_inds in names @@ -448,15 +448,15 @@ let fixpoint_message indexes l = | [] -> anomaly (Pp.str "no recursive definition.") | [id] -> Id.print id ++ str " is recursively defined" ++ (match indexes with - | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" - | _ -> mt ()) + | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" + | _ -> mt ()) | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ - spc () ++ str "are recursively defined" ++ - match indexes with - | Some a -> spc () ++ str "(decreasing respectively on " ++ - prvect_with_sep pr_comma pr_rank a ++ - str " arguments)" - | None -> mt ())) + spc () ++ str "are recursively defined" ++ + match indexes with + | Some a -> spc () ++ str "(decreasing respectively on " ++ + prvect_with_sep pr_comma pr_rank a ++ + str " arguments)" + | None -> mt ())) let cofixpoint_message l = Flags.if_verbose Feedback.msg_info (match l with diff --git a/interp/declare.mli b/tactics/declare.mli index 0f64235048..233f0674ec 100644 --- a/interp/declare.mli +++ b/tactics/declare.mli @@ -30,7 +30,7 @@ type variable_declaration = DirPath.t * section_variable_entry * logical_kind val declare_variable : variable -> variable_declaration -> Libobject.object_name -(** Declaration of global constructions +(** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) type constant_declaration = Evd.side_effects constant_entry * logical_kind @@ -58,7 +58,7 @@ val declare_constant : val declare_private_constant : ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects -val declare_definition : +val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> ?local:import_status -> Id.t -> ?types:constr -> constr Entries.in_universes_entry -> Constant.t diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 1861c5b99b..6dd749aa0d 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,3 +1,4 @@ +Declare Dnet Dn Btermdn |