aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2015-03-11CoqIDE: fix tag colors to support superposing unsafe and partialEnrico Tassi
Admitted (like Qed) can be "partially executed", but is also unsafe.
2015-03-11CoqIDE: restore module/proof name in info barEnrico Tassi
2015-03-11CoqIDE: do not lose tag on Qed ending focused proofEnrico Tassi
2015-03-11STM: ease re-editing of Admitted proofsEnrico Tassi
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
- no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
2015-03-09Do not display the status of monomorphic constants unless in ↵Guillaume Melquiond
universe-polymorphism mode.
2015-03-08Test for bug #2951.Pierre-Marie Pédrot
2015-03-08Fixing bug #2951.Pierre-Marie Pédrot
2015-03-07Test for #4035 (dependent destruction from Ltac).Hugo Herbelin
2015-03-07Reverting r10021 which enforces early assumptions on freshness whichHugo Herbelin
seem to be overly strong in practice (see discussion related to #4035).
2015-03-07Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar".Hugo Herbelin
Not inventing a new fresh name if a non-fresh name is explicitly given, as in v8.4.
2015-03-06Add some missing Proof keywords.Guillaume Melquiond
2015-03-06Simplify grammar for syntax highlighting by removing extraneous parentheses.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Print/Reset Extraction.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Extraction Inline and add Separate Extraction.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Extraction Language.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Typeclasses Opaque.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Module (Type).Guillaume Melquiond
2015-03-06Fix syntax highlighting of Extract Inductive.Guillaume Melquiond
2015-03-06Add syntax highlighting for Declare Module.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Import and Export.Guillaume Melquiond
2015-03-06Add syntax highlighting for Declare ML Module.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Require.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Scheme.Guillaume Melquiond
2015-03-06Do not highlight "using" as a constr keyword.Guillaume Melquiond
2015-03-06Add syntax highlighting for About.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Save.Guillaume Melquiond
2015-03-06Fix syntax highlighting of Hypothesis, Axiom, Variable, Parameter, and Context.Guillaume Melquiond
2015-03-06Add syntax highlighting for Coercion.Guillaume Melquiond
2015-03-06Fix syntax highlighting of "Require multiple libraries".Guillaume Melquiond
2015-03-06Merge branch 'v8.5' into trunkPierre Letouzey
2015-03-06MMapPositive: another implementation of MMapsPierre Letouzey
2015-03-05Fix testsuite with respect to the new formatting of Fail messages.Guillaume Melquiond
2015-03-05Preprend Fail to all the expected failures in the documentation.Guillaume Melquiond
This commit also removes comments from Coq examples, as they cause extraneous delayed prompts that clutter the output because coq_tex cannot remove them. Some documentation errors were also fixed in the process, since they are easier to spot now that only unexpected failures stand out.
2015-03-05Do not prepend a "Error:" header when the error is expected by the user.Guillaume Melquiond
This commit also removes the extraneous "=>" token from Fail messages and prevents them from losing all the formatting information.
2015-03-05Merge branch 'v8.5' into trunkPierre Letouzey
2015-03-05MMaps again : adding MMapList, an implementation by ordered listPierre Letouzey
2015-03-04Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-04Introducing MMaps, a modernized FMaps.Pierre Letouzey
NB: this is work-in-progress, there is currently only one provided implementation (MMapWeakList). In the same spirit as MSets w.r.t FSets, the main difference between MMaps and former FMaps is the use of a new version of OrderedType (see Orders.v instead of obsolete OrderedType.v). We also try to benefit more from recent notions such as Proper. For most function specifications, the style has changed : we now use equations over "find" instead of "MapsTo" predicates, whenever possible (cf. Maps in Compcert for a source of inspiration). Former specs are now derived in FMapFacts, so this is mostly a matter of taste. Two changes inspired by the current Maps of OCaml: - "elements" is now "bindings" - "map2" is now "merge" (and its function argument also receives a key). We now use a maximal implicit argument for "empty".
2015-03-04Introducing MMaps, a modernized FMaps.Pierre Letouzey
NB: this is work-in-progress, there is currently only one provided implementation (MMapWeakList). In the same spirit as MSets w.r.t FSets, the main difference between MMaps and former FMaps is the use of a new version of OrderedType (see Orders.v instead of obsolete OrderedType.v). We also try to benefit more from recent notions such as Proper. For most function specifications, the style has changed : we now use equations over "find" instead of "MapsTo" predicates, whenever possible (cf. Maps in Compcert for a source of inspiration). Former specs are now derived in FMapFacts, so this is mostly a matter of taste. Two changes inspired by the current Maps of OCaml: - "elements" is now "bindings" - "map2" is now "merge" (and its function argument also receives a key). We now use a maximal implicit argument for "empty".
2015-03-04Fix bug #3532, providing universe inconsistency information when aMatthieu Sozeau
unification fails due to that, during a conversion step.
2015-03-03Fix test-suite file, this is open.Matthieu Sozeau
2015-03-03Fix bug #3732: firstorder was using detyping to build existentialMatthieu Sozeau
instances and forgeting about the evars and universes that could appear there... dirty hack gone, using the evar map properly and avoiding needless constructions/deconstructions of terms.
2015-03-03Add missing test-suite files and update gitignore.Matthieu Sozeau
2015-03-03Add a test-suite file ensuring coinductives with primitive projectionsMatthieu Sozeau
do not enjoy eta-conversion and do not allow the usual failure of subject reduction in presence of dependent pattern-matching.
2015-03-03Fix test-suite file, this is currently a wontfix, but keep theMatthieu Sozeau
test-suite file for when we move to a better implementation.
2015-03-03Fix bug #3590, keeping evars that are not turned into named metas byMatthieu Sozeau
pattern_of_constr in an evar_map, as they can appear in the context of said named metas, which is used by change. Not sure what to do in the PEvar case, which never matches anyway according to Constr_matching.matches.
2015-03-03Improving display of camlp4/camlp5 versions, library and binary locations.Hugo Herbelin
2015-03-03Reinstalling search of camlpX in camldir, when given, forHugo Herbelin
compatibility with pre-1b7d4a033af heuristic in searching camlpX (continuation of a joint patch with Maxime). Typo basename -> dirname.
2015-03-03Typos in doc modules.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-05 04:20:50 +0000