aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* Removing two Pervasives.compare from Term.Gravatar ppedrot2013-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix for bug #3017: wrong handling of the unresolvability statusGravatar msozeau2013-04-03
| | | | | | | in clenvtac and error-printing code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16383 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Get rid of the LightenLibrary hack : no more last-minute collect of opaque terms and Obj.magic tricks. Instead, we make coqc accumulate the opaque terms as soon as constant_bodies are created outside sections. In these cases, the opaque terms are placed in a special table, and some (DirPath.t * int) are used as indexes in constant_body. In an interactive session, the local opaque terms stay directly stored in the constant_body. The structure of .vo file stays similar : magic number, regular library structure, digest of the first part, array of opaque terms. In addition, we now have a final checksum for checking the integrity of the whole .vo file. The other difference is that lazy_constr aren't changed into int indexes in .vo files, but are now coded as (substitution list * DirPath.t * int). In particular this approach allows to refer to opaque terms from another library. This (and accumulating substitutions in lazy_constr) seems to greatly help decreasing the size of opaque tables : -20% of vo size on the standard library :-). The compilation times are slightly better, but that can be statistic noise. The -force-load-proofs isn't active anymore : it behaves now just like -lazy-load-proofs. The -dont-load-proofs mode has slightly changed : opaque terms aren't seen as axioms anymore, but accessing their bodies will raise an error. Btw, API change : Declareops.body_of_constant now produces directly a constr option instead of a constr_substituted option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16382 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mod_subst.force: avoid using join when only one substGravatar letouzey2013-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16381 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor cleanup concerning Mod_subst.MBImapGravatar letouzey2013-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16380 85f007b7-540e-0410-9357-904b9bb8a0f7
* Exporting the SearchAbout filter.Gravatar ppedrot2013-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16379 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuation of r16346 on filtering local definitions. RefinedGravatar herbelin2013-03-30
| | | | | | | | | | | | the "choose less dependent" constraint-solving heuristic so that it is not disturbed by local definitions. This is a quick fix. A deeper analysis of the structure of constraints of the form ?x[args] = y, determining if variable y can itself be a local def or not, and whether args can be let-ins aliasing other variables, would allow to know if the fix needs to be refined further. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16376 85f007b7-540e-0410-9357-904b9bb8a0f7
* Safe_typing+Libary: use some arrays instead of lists in vo structuresGravatar letouzey2013-03-28
| | | | | | Very little space saved this way, but it would hurt either... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16375 85f007b7-540e-0410-9357-904b9bb8a0f7
* Safe_library : a record type for compiled_library instead of large tupleGravatar letouzey2013-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16374 85f007b7-540e-0410-9357-904b9bb8a0f7
* Synchronizing loadpath with the backtrack mechanism.Gravatar ppedrot2013-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16373 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved the Loadpath part of Library to its own file, and documentedGravatar ppedrot2013-03-26
| | | | | | the interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16372 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in refman (fix #2962)Gravatar letouzey2013-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16369 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enrich test-suite with a test for #2928Gravatar letouzey2013-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enrich test-suite with a test for #2734Gravatar letouzey2013-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16365 85f007b7-540e-0410-9357-904b9bb8a0f7
* Native compiler: hash-consing of generated code and values.Gravatar mdenes2013-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add the test-case of bug 2750 in the test-suiteGravatar letouzey2013-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16362 85f007b7-540e-0410-9357-904b9bb8a0f7
* Native compiler: timing info for reification in debug mode.Gravatar mdenes2013-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16357 85f007b7-540e-0410-9357-904b9bb8a0f7
* Native compiler: Inlined constants are now compiled, fixing a bug reported byGravatar mdenes2013-03-25
| | | | | | | Chantal Keller. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16356 85f007b7-540e-0410-9357-904b9bb8a0f7
* Normalized type for Vector.map2Gravatar pboutill2013-03-25
| | | | | | fix CoRN but there must be an underlying bug ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16355 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2989: make unification.ml able to deal with canonical structure in ↵Gravatar pboutill2013-03-25
| | | | | | | | any context + reindenting noise git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16354 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-05 04:50:44 +0000