diff options
| author | Emilio Jesus Gallego Arias | 2020-05-22 03:34:03 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-26 18:28:08 +0200 |
| commit | d9d4dcb41d8a63b7d535200b68bcbef4a38993df (patch) | |
| tree | bfb3c3cd7f27bf6634382b4003c3e362b7be4564 | |
| parent | baef9828c3e6ea11fce2e172797f0f67e51885ad (diff) | |
[declare] Turn restrict_ucontext hack into an internal parameter
This is not needed outside of `Declare` now.
| -rw-r--r-- | vernac/comFixpoint.ml | 2 | ||||
| -rw-r--r-- | vernac/declare.ml | 6 | ||||
| -rw-r--r-- | vernac/declare.mli | 3 |
3 files changed, 5 insertions, 6 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 80ca85e9a6..0b75e7f410 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -285,7 +285,7 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let fix_kind = Decls.IsDefinition fix_kind in let _ : GlobRef.t list = Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx - ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration + ~possible_indexes:indexes ~udecl ~ntns ~rec_declaration fixitems in () diff --git a/vernac/declare.ml b/vernac/declare.ml index 0c98ac9070..65f0265b3e 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -943,7 +943,7 @@ module Recthm = struct } end -let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = +let declare_mutually_recursive_core ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = let vars, fixdecls, indexes = mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in let uctx, univs = @@ -969,6 +969,8 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; csts +let declare_mutually_recursive = declare_mutually_recursive_core ~restrict_ucontext:true + let warn_let_as_axiom = CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ @@ -1540,7 +1542,7 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let udecl = UState.default_univ_decl in let kns = - declare_mutually_recursive ~scope ~opaque ~kind ~udecl ~ntns + declare_mutually_recursive_core ~scope ~opaque ~kind ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly ~restrict_ucontext:false fixitems in diff --git a/vernac/declare.mli b/vernac/declare.mli index 4e2ba1833f..5339f4702b 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -350,9 +350,6 @@ val declare_mutually_recursive -> ntns:Vernacexpr.decl_notation list -> rec_declaration:Constr.rec_declaration -> possible_indexes:lemma_possible_guards option - -> ?restrict_ucontext:bool - (** XXX: restrict_ucontext should be always true, this seems like a - bug in obligations, so this parameter should go away *) -> Recthm.t list -> Names.GlobRef.t list |