aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-04-18Fixed some printing bugs.herbelin
- Notations with coercions to funclass inserted were not working any longer since r11886. Made a fix but maybe should we eventually type the notations so that they have a canonical form (and in particular with coercions pre-inserted?). - Improved spacing management in printing extra tactic arguments "by" and "in". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12951 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-17A pass on the CHANGES file + credits for 8.3 (completing commit 12906herbelin
which involontarily propagated to the central repository a preliminary version of them). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12950 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-17Moved Case3.v from ideal features to success (it works since 8.2).herbelin
Two other tests are still "ideal features" though not failing (evars_subst.v is a complexity test still of bad complexity and universes.v just describes an improvement to do without checking anything). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12949 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-17Solved a few problems of auto by bypassing the call to apply.herbelin
Indeed, calling apply was inefficient (doing again a unification known to work) and moreover unsound (apply's unification is poorly tunable and the flags used in the first unification - in clenv_unique_resolve - were lost for apply). Solved the problem of still having a pretty acceptable user-friendly "info auto" by concealing the direct call to "clenv_refine" as a call to apply. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12948 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-17Use nice "unfold" instead of ugly "change" to display calls to unfold hintsherbelin
in "info auto". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12947 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-16cf. 12945soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12946 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-16Extraction: cosmetics when using ocaml + Extract Inductive to symbolsletouzey
- When using an infix constructor such as (::), whitespaces are to be given by the user, for instance Extract Inductive list => list [ "[]" "( :: )" ]. - Remove ugly whitespaces when using the ""-for-Pair trick: Extract Inductive prod => "(*)" [ "" ]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12944 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-16Extraction: restore (temporarily?) a very limited form of linear letin reductionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12943 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-16Extraction: less eta in calls to global functions, better optimization phaseletouzey
- we saturate the normalize function : as long as (kill_dummy + simpl) isn't a nop, we do it again. - generalize_case allowed on all types of theories/Init/*.v instead of only bool,sumbool,sumor. NB: this optim cannot be performed on any type, it might produce untyped code. - common_branch allowed on match with one branch: in this situation it indicates whether the match can be removed or not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12942 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-16Names.mli: double declaration of mind_modpathletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12941 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-16Extraction: improvement of optimizations (kill_dummy, optim_fix)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12940 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-16Util: remove list_split_at which is a clone of list_chopletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12939 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-16Extraction: ad-hoc identifier type with annotations for reductionsletouzey
* An inductive constructor Dummy instead of a constant dummy_name * The Tmp constructor indicates that the corresponding MLlam or MLletin is extraction-specific and can be reduced if possible * When inlining a glob (for instance a recursor), we tag some lambdas as reducible. In (nat_rect Fo Fs n), the head lams of Fo and Fs are treated this way, in order for the recursive call inside nat_rect to be correctly pushed as deeper as possible. * This way, we can stop allowing by default linear beta/let reduction even under binders (can be activated back via Set Extraction Flag). * Btw, fix the strange definition of non_stricts for (x y). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12938 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-16Compare_dec : a few better proofs (and extracted terms), some more Definedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12937 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-16Extraction: less _ in Haskell (typically for False_rect), less toplevel ↵letouzey
eta-expansions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12936 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-14Removing redundant internal variants of apply tactic and simplification of ↵herbelin
ML names (late consequences of commit r12603) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12934 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-13Remove only *.v.log files in clean of test-suite/Makefileglondu
...so that "./check > check.log" works as expected. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12933 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-11Look for csdp in $PATH at runtime, remove -csdpdir configure optionglondu
The csdp path computed by the configure script wasn't used at all, but was forcing presence of csdp at configure time whereas it is not used at all in the build process. Instead, we replace the configure-time check with a runtime check for existence of csdp in $PATH. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12929 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-11Remove unused functions run_sdpaglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12928 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-11Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12927 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Run parallelized test-suite in "check" target of main Makefileglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12926 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Prettier test-suite/Makefileglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12925 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Optimized need for delimiters when disjoint scopes for strings andherbelin
numerals are open (see e.g. part of bug report #2044). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12924 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Update .gitignoreglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12923 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Use the Makefile in test-suite/checkglondu
The output format is preserved, but not the dynamics (results are showed all at once at the end). This script could be removed altogether once the main Makefile (and daily bench) are fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12922 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Makefile for the test-suiteglondu
Using a Makefile for tests allows (easily) running them in parallel, running and/or benching a single one, adding depedencies between them, and running them with a version of Coq different than the one compiled with the current source tree. The new way to make statistics about successes/failures is also more reliable (I found bugs in the previous one). Statistics (on AMD Phenom(tm) 9950 Quad-Core Processor 2.6 GHz): - plain sh script: ~ 3 min - make -j6: ~ 1 min git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12921 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Fix typos in test-suite scriptglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12920 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Granting wish #2229 (InA_dec transparent) and Michael Day's coq-clubherbelin
8 April 2010 wish (addition of map_eq_nil). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12919 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Test for bug #2231 (unexpected error when using let/if over an inductiveherbelin
parameter in the type of a constructor). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12918 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Partially fixed bug #2231 (an inductive parameter name was internallyherbelin
used as a binding name in the return predicate of a Let/If case analysis causing a surprising error message; solved the problem by not checking for this kind of internal variables when the return predicate is anyway not given by the user; ideally, it should be detected that in the arguments of the inductive type, the parameter names can be reused w/o provoking captures - which are bad if the argument is implicit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12917 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-10Fixing various coqdep bugs (#2118, #2242, #2274)herbelin
- Made resolution of clashing -I options consistent with coqc (bug #2242) - Made semantics of -R consistent with the one introduced by revision 11188 in coqc, i.e. -R now makes visible all intermediate qualification levels (bug #2274) - Added support for -I -as and -R -as syntax - Extended escaping of special chars of GNU make and used escaping more systematically (bug #2118) - Made warnings follow English typography git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12916 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-09Change definition of FSetList so that equality is Leibnizglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12913 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-09Add test-suite/lia.cache to .gitignoreglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12912 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-09Fixing part 1 of bug #2242 (-I -as and -R -as were supported forherbelin
coqtop but not coqc). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12911 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-09Granting wish #2249 (checking existing lemma name also when in a section).herbelin
Simplified in passing generation of names for the "Goal" command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12910 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-09Documenting the use of ##, %%, $$ in coqdoc.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12909 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-09Applied Cédric Auger's patch to fix use of "#&xxx;" in html printingherbelin
rules (bug report #2293). Restored the sequential extension of the printing rules tables (that commit #12905 replaced by a per-file modification of the printing rules table). Note however that the table grows in the order of compilation of files by coqdoc, which does not necessarily coincide with the order of coqc compilation dependencies of the files. Added documentation of coqdoc option "--external". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12908 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-07Commit 12906 continued (forgotten file).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12907 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-07Granting wish #2251 thanks to commit 12900 solved bug 1416.v (whichherbelin
was actually failing for another reason than the reason originally filled in the bug tracker) and revealed a bug in the unification.v test file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12906 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-06New model for user-driven translation of tokens in coqdocherbelin
In the initial model (formerly to r11432), coqdoc parsed separatedly letters and symbolic characters and was thus not able to translate tokens mixing letters and symbolic characters such as "\in" or "=_h". Revision 11432 extended the definition of translatable tokens by supporting letters in it with the benefit of supporting "\in" or "=_h" but added the constraint of requiring spaces to correctly separate tokens in expressions such as "x : nat" which otherwise would be split into "x" and ":nat", then leading to fail understanding "nat" as a proper reference. The new model renounces to define a lexical category of tokens and uses instead a dynamically extensible sublexer similar to the one used in the Coq lexer. The new model works even if tokens are not separated by spaces in the source file and it thus solves problems such as the one mentioned in bug #2273 (failure to link C in "`(!C)"). However, it imposes a stronger discipline in writing the lexing rules in cpretty.mll because the characters that can eventually contribute to the application of a printing rule are buffered in the sublexer and no output is allowed to occur until the buffer of the sublexer if flushed. The theoretical overhead due to the intermediate use of buffers is apparently less than 5%. More details on the token cutting discipline can be found in the new file token.mli. Incidentally fixed two small problems with notation links in LaTeX: made escaping of characters in LaTeX labels more robust so that notations do not easily get the same label name; avoid only highlighting the first '"' of a notation def (failing to have now a better highlighting strategy). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12905 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-05Improving compatibility between 8.2 and 8.3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12904 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-05Fix configure script: natdynlink works without a hack on 10.6.3.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12903 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-05Added a function in typing.ml to solve evars of a constr w/o going back down ↵herbelin
to rawconstr Also cleaned a bit typing.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12902 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-05Changement de ide/proofs.ml en ide/ideproofs.ml pour éviter un conflitaspiwack
avec le futur commit de la nouvelle machinerie de preuve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12901 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-05Granting wish #2251 (forbidding rewriting a term reduced to an evar)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12900 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-05Tests for bug report #2244 (pattern-unification with abstraction over Meta's)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12899 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-05Partial fix to bug #2244 (ensure that pattern unification does notherbelin
abstract over Meta's by first posing the Meta's as Evar's). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12898 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-31Add documentation on the treatment of [if] and [let (x1, ... xn) := ..]msozeau
by Program. Fix some broken examples and detail the syntax of order annotations for well-founded recursion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12897 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-30Small things about coqdoc + fixing lettuple.v test (part of bug #2289)herbelin
In coqdoc, made links to utf8 notations working and made representation of locations for notations more compact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12896 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-30Removed hard-wiring of latin1 letters in coqdoc (see bug #2275)herbelin
(it interfered badly with utf-8: just take an utf-8 like "forall" which starts in iso-8859-1 with a "a circonflex"; nothing is lost since intentedly iso-8859-1 chars can only occur in comments and there is no ident detection in comments) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12895 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:14:33 +0000