aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 12)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16288 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 11)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16287 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 10)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16286 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 9)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16285 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 7)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16283 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 6)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16282 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 5)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16281 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 4)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16280 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Implicit_quantifiers.is_freevar: cleaner, no more try...with _ ->...letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16279 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 3)letouzey
NB: this "try...with" plus the test at the next line (if !interning_grammar || env.unb then ...) were actually catching too many errors (for instance error_not_enough_arguments). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16278 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 2)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16277 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 1)letouzey
Why? : avoid catching (and probably ignoring) exceptions such as Sys.Break, anomalies, assertions, leading to undetected bugs and ignored Ctrl-C. How? : when the precise exception(s) concerned by the try is known, use them explicitely in the "with". Otherwise, let's use the pattern "with e when Errors.noncritical e -> " Particular case : when an exception is catched and reraised immediately after some adjustments, we leave it untouched. Simply, for easily identifying these situations later, the name of the exception variable is changed to "reraise". Please also adopt this coding style. Automatic checks based on the "mascot" tool of X. Clerc will be runned regularly. If you want to avoid to check a particular try...with, use the variable name "any" after the "with". All these changes have been tested using the standard library and the test-suite, but unfortunately this is far from ensuring that coqtop behaves as before. We'll see after the nightly bench... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16276 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Hipattern : consider jmeq only when Logic.JMeq is loadedletouzey
Otherwise an Anomaly coming from Coqlib.find_reference is raised and catched for the moment, but that will change soon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16275 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12A version of Univ.check_eq with no anomaly for Evd.set_eq_sortletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16274 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Equality: avoid an anomaly about inj_pair2_eq_decletouzey
In coming commits, we'll restrict (try ... with ...), in particular to avoid catching anomalies. Currently, an anomaly about inj_pair2_eq_dec is raised and catched, let's avoid that by ensuring that Eqdep_dec is loaded before entering the critical code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16273 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Recdef: an anomaly isn't so anomalous, occurs in 1618.vletouzey
For the moment, this anomaly is catched and ignore later, but that will changed soon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16272 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Term.dest* functions now raise specific DestKO exn instead of Invalid_argumentletouzey
**Warning** the ml code of plugins may have to be adapted after this. Concerning coq itself, I've done the adaptations, let's hope I've forgotten none. In practice, the number of changes are relatively low, and the code is quite cleaner this way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16271 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12New function Errors.noncritical for restricting try ... with ...letouzey
For the moment, are considered critical : Sys.Break, Stack_overflow, Out_of_memory Assert_failure, Match_failure, Anomaly, Timeout, Drop, Exit These exceptions should normally *not* be catched by a "try", hence the suggested code for generic "try": try ... with e when Errors.noncritical e -> ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16269 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Updated Exninfo to the new Store type.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16268 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Allowing different types of, not to be mixed, generic Stores throughppedrot
functor application. Rewritten the interface btw. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16267 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-11Allowing (Co)Fixpoint to be defined local and Let-style.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16266 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-11Obligations generated by Program are now local.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16265 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-11Documentation of the "Local Definition" command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16264 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
has to be refered through its qualified name even when the module containing it is imported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16263 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-08catch failures of pr_vernac to make -time failsafegareuselesinge
Printing Ltac code is broken. This was not compiling with -time Ltac pop_succn e := eval lazy beta iota delta [plus] in (1 + 1). The bug in the pretty printer should be fixed too... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16262 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-08Use with_state_protection in pr_module_vardeclsgareuselesinge
This makes pr_module_vardecls side effect free, as any pp function should be git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16261 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-05More monomorphization.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-05Missing primitive in CArrayppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16259 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-28compare_stack_shape before ise_stack2 in evar_convpboutill
+ revert r16130 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16258 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-28Repairing r16205: errors raised by check_evar_instance were no longerherbelin
trapped by solve_simple_eqn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16257 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-28More informative error when a global reference is used in a context ofherbelin
local variables which is a different from the one of its definition. E.g.: Section A. Variable n:nat. Definition c:=n. Goal True. clear n. Check c. [I'm however unsure that "n" should not continue to be accessible via some global (qualified) name, even after the "clear n".] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16256 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-27Coqlib: minor simplificationsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16255 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-27Update debug code according to reorganization into modules.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16254 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-27Minor cleanup around Term_typingletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16253 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-27remove a warning after Drop about print_hint_dbletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16252 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-27Adapt dev/base_include to new Declarationsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16251 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-26kernel/declarations becomes a pure mliletouzey
- constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml - the functions that were in declarations.ml (mostly substitution utilities and hashcons) are now in kernel/declareops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16249 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-26Names: Modularize constant and mutual_inductiveletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16248 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-26Mod_subst: misc reformulationsletouzey
* Remove the mind_of_delta and constant_of_delta functions, prefer instead the {mind,constant}_of_delta_kn functions. * Attempt to make subst_ind and subst_con0 more self-contained git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16247 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-25cbn friendly VectorDefpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16245 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-25Evarconv: When doing a iota of a fixpoint, use constant name instead of ↵pboutill
fixpoint definition + Help the use of #trace on evar_conv_appr_x git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16244 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-25CoqIDE: Add TAB key to autocompleteppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16243 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-24Fixing bug #2466ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16241 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-24New -no-native-compiler flag for configure, globally disabling the nativemdenes
compiler (implemented on Matthieu's request). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16240 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-24Reduced the noise level when dynlinking in bytecode mode or whenmdenes
-no-native-compiler flag is on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16239 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-22Tentative heuristic fix to handle lexer failures from CoqIDE whenppedrot
cutting XML phrases carelessly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16238 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-22Cosmetic changes to CoqIDE finder widget.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16237 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 22:15:51 +0000