aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* cbn can be called by EvalGravatar pboutill2013-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16353 85f007b7-540e-0410-9357-904b9bb8a0f7
* Comments in mliGravatar pboutill2013-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake*: avoid some warning about Let outside sectionsGravatar letouzey2013-03-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16350 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug# 2994, 2971 about better error messages.Gravatar msozeau2013-03-22
| | | | | | | Fix bug# 2956, porting fix from 8.4 branch git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16349 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing unfolding of local definitions during unification that appearedGravatar herbelin2013-03-21
| | | | | | | | | with commit r16233. This commit added a more precise filtering of variables on which an evar was allowed to be dependent, but) but it also broke some Ssreflect scripts. The reason why that filtering was incorrectly applied, sometimes, to local definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16346 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.Gravatar herbelin2013-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16344 85f007b7-540e-0410-9357-904b9bb8a0f7
* Robust display of NotConvertibleTypeField errors (fix #3008, #2995)Gravatar letouzey2013-03-21
| | | | | | | | | | | | | | Since the nametab isn't aware of everything needed to print mismatched types (cf the bug test-cases), we create a robust term printer that known how to print a fully-qualified name when [shortest_qualid_of_global] has failed. These Printer.safe_pr_constr and alii are meant to never fail (at worse they display "??", for instance when the env isn't rich enough). Moreover, the environnement may have changed between the raise of NotConvertibleTypeField and its display, so we store the original env in the exception. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16342 85f007b7-540e-0410-9357-904b9bb8a0f7
* Firstorder: record with defined field aren't conjonctions (fix #2629)Gravatar letouzey2013-03-21
| | | | | | | | | | | | | | The let-in in the type of constructor was perturbating the Hipattern.dependent check, leading firstorder to consider too much inductives as dependent-free conjonctions, ending with lift errors (UNBOUND_REL_-2, ouch). This patch is probably overly cautious : if the variable of the let-in is used, we consider the constructor to be dependent. If someday somebody feels it necessary, he/she could try to reduce the let-in's instead... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16339 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using hnf instead of "intro H" for forcing reduction to a product.Gravatar herbelin2013-03-21
| | | | | | | | Added full betaiota in hnf. This seems more natural, even if it changes the strict meaning of hnf. This is source of incompatibilities as "intro" might succeed more often. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16338 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing an old pecularity of "red": head betaiota redexes are nowGravatar herbelin2013-03-21
| | | | | | reduced in order to find some head constant to reduce. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo dans message d'erreur (obligations).Gravatar herbelin2013-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16336 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add type information in error message when a constructor is not fullyGravatar herbelin2013-03-21
| | | | | | | | | applied in pattern-matching. This provides with a side way for the user to understand what is happening in the situation match ... with ... S ... => ... end" where S is supposed to be a variable but S being taken by Coq as successor in nat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16335 85f007b7-540e-0410-9357-904b9bb8a0f7
* Check unexpected "Local" keyword in cmd before opening a proof (fix #2975)Gravatar letouzey2013-03-21
| | | | | | | | This fix isn't ideal. Instead, something like States.with_heavy_rollback should be able to cancel a proof started during a command interp that failed. But anyway, "le mieux est l'ennemi du bien"... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16333 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing mandatory suffixes for library files.Gravatar ppedrot2013-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7
* Printmod: handle more examples thanks to better nametab useGravatar letouzey2013-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16329 85f007b7-540e-0410-9357-904b9bb8a0f7
* Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)Gravatar letouzey2013-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16328 85f007b7-540e-0410-9357-904b9bb8a0f7
* Check a list length before doing a List.chop (fix #3000)Gravatar letouzey2013-03-20
| | | | | | | I'm not completely sure that raising Not_found is the right thing to do here, but it seems reasonable... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16326 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better encapsulation of MessageViewGravatar ppedrot2013-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using ML signalling in CoqIDEGravatar ppedrot2013-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16322 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding color for warnings in CoqIDEGravatar ppedrot2013-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16321 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing the module Libtypes and unifying the Search[Pattern|Rewrite]?Gravatar ppedrot2013-03-19
| | | | | | | | | | | | | | | | mechanism with the SearchAbout one. Searches may be slower, but this is unlikely to be noticed. In addition, according to Hugo, the Libtype summary was imposing a noticeable time penalty without any real advantage. Now Search and SearchPattern are the same. The documentation was not really clear about the difference between both, except that Search was restricted to closed terms. This is an artificial restriction by now. Fixing #2815 btw. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16320 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix for bug #3004 (thanks Hugo!)Gravatar letouzey2013-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16317 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction AccessOpaque is now activated again by default (#2952)Gravatar letouzey2013-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16315 85f007b7-540e-0410-9357-904b9bb8a0f7
* Making local variable warning verbose by default.Gravatar ppedrot2013-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16314 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ppvernac: no globalization for printing ltac definitionsGravatar letouzey2013-03-17
| | | | | | | | | | | | | | | This way, ppvernac is entirely at the "raw" level : constr_expr, raw_tactic_expr, ... Using globalization for ltac was awkward since it was the only such place handled this way. Moreover the env necessary for pr_glob_tactic was possibly wrong (cf last commit concerning module params), and the pr_glob_tactic was raising exceptions from time to time (typically on a "eval ..." ltac raising a "tactic expected"). Feel free to revert if this globalization has indeed an interest I missed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16312 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix some camlp5 quotations , restoring compatibility with camlp5 5.xGravatar letouzey2013-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16311 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker: simplify a bit its exception handlerGravatar letouzey2013-03-17
| | | | | | | | We use Errors.print for anomalies and other uncaught exceptions in the checker: this should print the same message, it is shorter this way, and we avoid using Errors.is_anomaly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16310 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid a few overzealous "when Errors.noncritical"Gravatar letouzey2013-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16309 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retyping.get_type_of: a lax version raising no anomaliesGravatar letouzey2013-03-17
| | | | | | | | | | | | | | | | | | | | | | There are at least two situations (in Evarsolve and Pretyping) where Retyping.get_type_of may be called on ill-typed terms, leading to possible anomalies that used to be immediately catched and discarded. Instead, retyping.get_type_of now has an extra optional arg ~lax that makes it fail with a regular exception instead of anomalies. Of course, it would be best someday to be able to avoid using get_type_of on possibly ill-typed terms... If somebody wants to investigate this: - example that leads the get_type_of in Pretyping to a failure: test-suite/succes/ltac.v - example that leads the get_type_of in Evarsolve to a failure: MathClasses/implementations/list.v, a rewrite line 42 (* :-) *) cf bench failure on 2013-3-15. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16308 85f007b7-540e-0410-9357-904b9bb8a0f7
* another Errors.push in a exception reraiseGravatar letouzey2013-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16307 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extract_env : correct exceptions mentionned in a try ... withGravatar letouzey2013-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16306 85f007b7-540e-0410-9357-904b9bb8a0f7
* Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncriticalGravatar letouzey2013-03-14
| | | | | | | This was apparently already the case before, but this invariant is now explicited in comments + a few asserts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16305 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cerrors: get rid of some FIXMEGravatar letouzey2013-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16304 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in an error messageGravatar letouzey2013-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16303 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use Pp.msg instead of Pp.pp in -beautify (loss of text otherwise)Gravatar letouzey2013-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pptactic.pr_raw_tactic is now without env argumentGravatar letouzey2013-03-14
| | | | | | | 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
* Modules and ppvernac, sequel of Enrico's commit 16261Gravatar letouzey2013-03-13
| | | | | | | | | | | | 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
* Declaremods: a few syntactic improvementsGravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16299 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made the backtrace type opaqueGravatar ppedrot2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16298 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation of coqchk (broken by commit 16268), bis repetitaGravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16297 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation of coqchk (broken by commit 16268)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16296 85f007b7-540e-0410-9357-904b9bb8a0f7
* Toplevel: improved commentsGravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vernac+Toplevel: get rid of Error_in_fileGravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16294 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vernac+Toplevel: get rid of DuringVernacInterpGravatar letouzey2013-03-13
| | | | | | | | | 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
* Restrict (try...with...) to avoid catching critical exn (part 15)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16292 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 14)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16291 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16289 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16288 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 03:34:56 +0000