aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-04-15Checker: empty sections hardcoded in cb and mindletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16400 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-15Checker: reified encoding of .vo types in values.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16399 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-15Checker: regroup all vo-related types in cic.mliletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16398 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-15anew_instance should not consume the locality twicegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16397 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
This commit introduces 2 new vernac_expr constructors: - VernacLocal (b,v) that represents a vernacular v with the "Local" modifier - VernacProgram v that represents a vernacular v with the "Program" modifier This allows the parser to avoid using side effects to model the two modifiers, that are now represented in the AST. This also decouples the parsing phase from the interpretation phase, since parsing a second phrase does not alter the locality flag for the first phrase. As a consequence all the locality_flag components of vernac_expr have been removed, but for the ones that (for retro compatibility) allow an "infix" Local flag. In these cases the boolean is renamed obsolete_locality (as the grammar entry that parses it), and during interpretation we check that at most one locality flag is specified, using the idiom (where the input local is the obsolete one): let local = enforce_XXX_locality locality local in Another improvement is that the default locality is not chosen in the parser, but in the interpreter where the idiom let local = make_XXX_locality locality in is used to default the locality to XXX (module/section/whatever). Unfortunately not all side effects have been removed: - Flags.program_mode is still used to signal that we are in program mode - Locality.LocalityFixme.* functions are used in commands that do not have an AST, but are parsed as VernacExtend (see vernacinterp.ml) I guess one could fix the latter case systematically adding an extra argument "locality" to commands attached using VERNAC COMMAND EXTEND. Fixing plugins adding commands that honour "Local" should look like this: VERNAC COMMAND EXTEND Set_Solver | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ set_default_tactic - (Locality.use_section_locality ()) + (Locality.make_section_locality (Locality.LocalityFixme.consume ())) (Tacintern.glob_tactic t) ] END In any case the side effects are set/consumed within then interpretation phase, and not set during the parsing phase and consumed during the interpretation phase. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16396 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-11Backport r16394 from 8.4:msozeau
- Fix caching of local hint database in typeclasses eauto which could miss some hypotheses. - Fix automatic solving of obligation in program, which was not trying to solve obligations that had no undefined dependencies left. Fix a warning in fourierR.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16395 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-10Equality: avoid some unprotected List.nth (fix #2837)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16392 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-09Added a module of immutable arrays. Not as full as CArray, but shouldppedrot
be soon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16391 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-08Enrich test-suite with a test for #3022.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16390 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-05Allow catching of WrongAbstractionType, fixing a regression from 8.4msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16389 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-04Small doc fix : module subtyping cannot force access of opaquesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16385 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-03Removing two Pervasives.compare from Term.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16384 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-03Fix for bug #3017: wrong handling of the unresolvability statusmsozeau
in clenvtac and error-printing code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16383 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
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
2013-04-02Mod_subst.force: avoid using join when only one substletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16381 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-02Minor cleanup concerning Mod_subst.MBImapletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16380 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-02Exporting the SearchAbout filter.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16379 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-30Continuation of r16346 on filtering local definitions. Refinedherbelin
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
2013-03-28Safe_typing+Libary: use some arrays instead of lists in vo structuresletouzey
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
2013-03-28Safe_library : a record type for compiled_library instead of large tupleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16374 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-26Synchronizing loadpath with the backtrack mechanism.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16373 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-26Moved the Loadpath part of Library to its own file, and documentedppedrot
the interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16372 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Typo in refman (fix #2962)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16369 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Enrich test-suite with a test for #2928letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16367 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Enrich test-suite with a test for #2734letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16365 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Native compiler: hash-consing of generated code and values.mdenes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16363 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Add the test-case of bug 2750 in the test-suiteletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16362 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Native compiler: timing info for reification in debug mode.mdenes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16357 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Native compiler: Inlined constants are now compiled, fixing a bug reported bymdenes
Chantal Keller. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16356 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Normalized type for Vector.map2pboutill
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
2013-03-25Fix bug #2989: make unification.ml able to deal with canonical structure in ↵pboutill
any context + reindenting noise git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16354 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25cbn can be called by Evalpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16353 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25 Comments in mlipboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16352 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-23Minor code cleaning in CArray / CList.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-22NMake*: avoid some warning about Let outside sectionsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16350 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-22Fix bug# 2994, 2971 about better error messages.msozeau
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
2013-03-21Fixing unfolding of local definitions during unification that appearedherbelin
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
2013-03-21Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16344 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Robust display of NotConvertibleTypeField errors (fix #3008, #2995)letouzey
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
2013-03-21Firstorder: record with defined field aren't conjonctions (fix #2629)letouzey
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
2013-03-21Using hnf instead of "intro H" for forcing reduction to a product.herbelin
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
2013-03-21Fixing an old pecularity of "red": head betaiota redexes are nowherbelin
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
2013-03-21Typo dans message d'erreur (obligations).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16336 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Add type information in error message when a constructor is not fullyherbelin
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
2013-03-21Check unexpected "Local" keyword in cmd before opening a proof (fix #2975)letouzey
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
2013-03-21Removing mandatory suffixes for library files.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Printmod: handle more examples thanks to better nametab useletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16329 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16328 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-20Check a list length before doing a List.chop (fix #3000)letouzey
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
2013-03-20Better encapsulation of MessageViewppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16323 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:54:14 +0000