diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 6 | ||||
| -rw-r--r-- | vernac/record.ml | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 19 | ||||
| -rw-r--r-- | vernac/vernacprop.ml | 17 | ||||
| -rw-r--r-- | vernac/vernacprop.mli | 2 |
5 files changed, 17 insertions, 28 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 6914f899b7..4a2dba859f 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -69,8 +69,7 @@ let existing_instance glob g info = let instance, _ = Global.type_of_global_in_context (Global.env ()) c in let _, r = Term.decompose_prod_assum instance in match class_of_constr Evd.empty (EConstr.of_constr r) with - | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob - (*FIXME*) (Flags.use_polymorphic_flag ()) c) + | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c) | None -> user_err ?loc:(loc_of_reference g) ~hdr:"declare_instance" (Pp.str "Constant does not build instances of a declared type class.") @@ -393,8 +392,7 @@ let context poly l = let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in match class_of_constr sigma (of_constr t) with | Some (rels, ((tc,_), args) as _cl) -> - add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*) - poly (ConstRef cst)); + add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (ConstRef cst)); status (* declare_subclasses (ConstRef cst) cl *) | None -> status diff --git a/vernac/record.ml b/vernac/record.ml index d9dc16d96e..1e464eb8bf 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -531,6 +531,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari match univs with | Polymorphic_const_entry univs -> let usubst, auctx = Univ.abstract_universes univs in + let usubst = Univ.make_instance_subst usubst in let map c = Vars.subst_univs_level_constr usubst c in let fields = Context.Rel.map map fields in let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index aa6121c39a..ded0d97e64 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2132,10 +2132,6 @@ let check_vernac_supports_polymorphism c p = | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> () | Some _, _ -> user_err Pp.(str "This command does not support Polymorphism") -let enforce_polymorphism = function - | None -> Flags.is_universe_polymorphism () - | Some b -> Flags.make_polymorphic_flag b; b - (** A global default timeout, controlled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) @@ -2202,6 +2198,7 @@ let with_fail st b f = end let interp ?(verbosely=true) ?proof ~st (loc,c) = + let orig_univ_poly = Flags.is_universe_polymorphism () in let orig_program_mode = Flags.is_program_mode () in let rec control = function | VernacExpr v -> @@ -2213,8 +2210,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = control v | VernacRedirect (s, (_,v)) -> Topfmt.with_output_to_file s control v - | VernacTime (_,v) -> - System.with_time !Flags.time control v; + | VernacTime (batch, (_loc,v)) -> + System.with_time ~batch control v; and aux ?polymorphism ~atts isprogcmd = function @@ -2241,7 +2238,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = | c -> check_vernac_supports_locality c atts.locality; check_vernac_supports_polymorphism c polymorphism; - let polymorphic = enforce_polymorphism polymorphism in + let polymorphic = Option.default (Flags.is_universe_polymorphism ()) polymorphism in + Flags.make_universe_polymorphism polymorphic; Obligations.set_program_mode isprogcmd; try vernac_timeout begin fun () -> @@ -2249,9 +2247,12 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = if verbosely then Flags.verbosely (interp ?proof ~atts ~st) c else Flags.silently (interp ?proof ~atts ~st) c; + (* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`, + we should not restore the previous state of the flag... *) if orig_program_mode || not !Flags.program_mode || isprogcmd then Flags.program_mode := orig_program_mode; - ignore (Flags.use_polymorphic_flag ()) + if (Flags.is_universe_polymorphism() = polymorphic) then + Flags.make_universe_polymorphism orig_univ_poly; end with | reraise when @@ -2262,8 +2263,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = let e = CErrors.push reraise in let e = locate_if_not_already ?loc e in let () = restore_timeout () in + Flags.make_universe_polymorphism orig_univ_poly; Flags.program_mode := orig_program_mode; - ignore (Flags.use_polymorphic_flag ()); iraise e in if verbosely diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 4a01ef2efa..4fdc78dd2a 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -14,14 +14,14 @@ open Vernacexpr let rec under_control = function | VernacExpr c -> c | VernacRedirect (_,(_,c)) - | VernacTime (_,c) + | VernacTime (_,(_,c)) | VernacFail c | VernacTimeout (_,c) -> under_control c let rec has_Fail = function | VernacExpr c -> false | VernacRedirect (_,(_,c)) - | VernacTime (_,c) + | VernacTime (_,(_,c)) | VernacTimeout (_,c) -> has_Fail c | VernacFail _ -> true @@ -38,7 +38,7 @@ let is_navigation_vernac c = is_navigation_vernac_expr (under_control c) let rec is_deep_navigation_vernac = function - | VernacTime (_,c) -> is_deep_navigation_vernac c + | VernacTime (_,(_,c)) -> is_deep_navigation_vernac c | VernacRedirect (_, (_,c)) | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c | VernacExpr _ -> false @@ -53,17 +53,6 @@ let is_debug cmd = match under_control cmd with | VernacSetOption (["Ltac";"Debug"], _) -> true | _ -> false -let is_query cmd = match under_control cmd with - | VernacChdir None - | VernacMemOption _ - | VernacPrintOption _ - | VernacCheckMayEval _ - | VernacGlobalCheck _ - | VernacPrint _ - | VernacSearch _ - | VernacLocate _ -> true - | _ -> false - let is_undo cmd = match under_control cmd with | VernacUndo _ | VernacUndoTo _ -> true | _ -> false diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli index eb7c7055ac..df739f96a9 100644 --- a/vernac/vernacprop.mli +++ b/vernac/vernacprop.mli @@ -21,6 +21,6 @@ val has_Fail : vernac_control -> bool val is_navigation_vernac : vernac_control -> bool val is_deep_navigation_vernac : vernac_control -> bool val is_reset : vernac_control -> bool -val is_query : vernac_control -> bool val is_debug : vernac_control -> bool val is_undo : vernac_control -> bool + |