aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-03-14Typo in an error messageletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16303 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-14Use Pp.msg instead of Pp.pp in -beautify (loss of text otherwise)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16302 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-14Pptactic.pr_raw_tactic is now without env argumentletouzey
This env argument was just there by analogy with the glob_tactic case, and actually ignored for raw_tactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16301 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
After some investigation, I see no reason to try to hack the nametab in ppvernac, since everything happens there at a lower level (constr_expr). So the offending code that Enrico protected with a State.with_state_protection is now gone. By the way, moved some types from Declaremods to Vernacexpr to avoid some dependencies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16300 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Declaremods: a few syntactic improvementsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16299 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Made the backtrace type opaqueppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16298 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Fix compilation of coqchk (broken by commit 16268), bis repetitaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16297 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Fix compilation of coqchk (broken by commit 16268)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16296 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Toplevel: improved commentsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16295 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Vernac+Toplevel: get rid of Error_in_fileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16294 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Vernac+Toplevel: get rid of DuringVernacInterpletouzey
This meta-exception was already almost unused, just to distinguish exceptions during parsing or interp. Some code cleanup btw git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16293 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 15)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16292 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 14)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16291 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7
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@16289 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 01:46:37 +0000