diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 12 | ||||
| -rw-r--r-- | engine/evd.mli | 12 | ||||
| -rw-r--r-- | engine/proofview.ml | 18 | ||||
| -rw-r--r-- | engine/univGen.ml | 6 | ||||
| -rw-r--r-- | engine/univGen.mli | 3 |
5 files changed, 22 insertions, 29 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 8e7d942c37..70f58163fd 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -902,14 +902,14 @@ let make_nonalgebraic_variable evd u = let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s = with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s) -let fresh_constant_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c) +let fresh_constant_instance ?loc ?(rigid=univ_flexible) env evd c = + with_context_set ?loc rigid evd (UnivGen.fresh_constant_instance env c) -let fresh_inductive_instance ?loc env evd i = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i) +let fresh_inductive_instance ?loc ?(rigid=univ_flexible) env evd i = + with_context_set ?loc rigid evd (UnivGen.fresh_inductive_instance env i) -let fresh_constructor_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c) +let fresh_constructor_instance ?loc ?(rigid=univ_flexible) env evd c = + with_context_set ?loc rigid evd (UnivGen.fresh_constructor_instance env c) let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr = with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr) diff --git a/engine/evd.mli b/engine/evd.mli index 8843adc853..82e1003a65 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -653,10 +653,14 @@ val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t -val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant -val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive -val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid + -> evar_map -> Sorts.family -> evar_map * Sorts.t +val fresh_constant_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> Constant.t -> evar_map * pconstant +val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> inductive -> evar_map * pinductive +val fresh_constructor_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> constructor -> evar_map * pconstructor val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> GlobRef.t -> evar_map * econstr diff --git a/engine/proofview.ml b/engine/proofview.ml index 16be96454e..b0ea75ac60 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -302,7 +302,8 @@ let tclONCE = Proof.once exception MoreThanOneSuccess let _ = CErrors.register_handler begin function - | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.") + | MoreThanOneSuccess -> + Pp.str "This tactic has more than one success." | _ -> raise CErrors.Unhandled end @@ -347,8 +348,7 @@ exception NoSuchGoals of int let _ = CErrors.register_handler begin function | NoSuchGoals n -> - CErrors.user_err - (str "No such " ++ str (String.plural n "goal") ++ str ".") + str "No such " ++ str (String.plural n "goal") ++ str "." | _ -> raise CErrors.Unhandled end @@ -420,12 +420,9 @@ let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t = exception SizeMismatch of int*int let _ = CErrors.register_handler begin function | SizeMismatch (i,j) -> - let open Pp in - let errmsg = - str"Incorrect number of goals" ++ spc() ++ - str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")." - in - CErrors.user_err errmsg + let open Pp in + str"Incorrect number of goals" ++ spc() ++ + str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")." | _ -> raise CErrors.Unhandled end @@ -910,7 +907,8 @@ let tclPROGRESS t = tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress.")) let _ = CErrors.register_handler begin function - | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | Logic_monad.Tac_Timeout -> + Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!" | _ -> raise CErrors.Unhandled end diff --git a/engine/univGen.ml b/engine/univGen.ml index 1fe09270ba..b270f9dc0b 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -48,8 +48,6 @@ let fresh_instance_from ?loc ctx = function (** Fresh universe polymorphic construction *) -open Globnames - let fresh_global_instance ?loc ?names env gr = let auctx = Environ.universes_of_global env gr in let u, ctx = fresh_instance_from ?loc auctx names in @@ -78,10 +76,6 @@ let constr_of_monomorphic_global gr = Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ str " would forget universes.") -let fresh_global_or_constr_instance env = function - | IsConstr c -> c, ContextSet.empty - | IsGlobal gr -> fresh_global_instance env gr - let fresh_sort_in_family = function | InSProp -> Sorts.sprop, ContextSet.empty | InProp -> Sorts.prop, ContextSet.empty diff --git a/engine/univGen.mli b/engine/univGen.mli index 1b351c61c4..bbde9d4e30 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -46,9 +46,6 @@ val fresh_constructor_instance : env -> constructor -> val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t -> constr in_universe_context_set -val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> - constr in_universe_context_set - (** Get fresh variables for the universe context. Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) val fresh_universe_context_set_instance : ContextSet.t -> |