aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-07-29Tacred: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14317 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Hipattern: two generic equalities on constr spotted & rewrittenpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14316 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Indtypes: remove useless and wrong generic equality test on constr arraypuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14315 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Term: slight reorganization of the filepuech
- removed duplicate constructors - moved code around for more clarity git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14314 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Term_typing, Typeops: replace some generic '=' on constr by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14313 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Term: Refactoring of hashconsingpuech
- moved the alterate Hashtable module to a separate file - moved all hashconsing-related function to a separate section in Term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14312 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29argument renaming in liftn (match with usual terminology)puech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14311 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-28Ide_slave: same attributes for { } and Focus/Unfocus (fix coqide display)letouzey
Without this, coqide display a copy of the goal in its response buffer... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14310 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-27Coqide: GEdit.combo is deprecated since Gtk2.4! We now use ↵pboutill
GEdit.combo_box_entry_text git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14306 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-27Oversight in revision 14292.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14305 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-27Typo of bug 2577pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14303 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26or_introl is now too complicated for basic tests of ↵pboutill
test-suite/output/PrintInfos.v This is due to r14296. existT should do the job. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14302 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26Partial revert of r14292pboutill
No more assertion failure because of half done job. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14301 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26ide/coq_lex.mll: restore the separate parsing of .. (fix #2578)letouzey
Trying to have a direct rule for "..." seemed to be less hack-ish, but is in fact _wrong_, shame on me : it's important to have a rule for ".." since this can appear in a coq sentence (for instance in recursive notations), and hence we don't want the second dot to be considered as a terminator. So let's restore the previous situation, with a rule for ".." (ignoring them) and a rule for "."+blank. Then "..." is recognized as ".." + ".", which is quite ok after all. The fact that ".. ." is also recognized by coqide in a similar way isn't actually a problem: after reading this sentence, coqide will send it to coqtop, and it's coqtop that will tell that this sentence makes no sense... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14300 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26Integral domainspottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14299 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26Ring2 devient Ncring et la reification par les type classes est partageepottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14298 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26All the parameters of Compare are implicits.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14297 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26All the parameters of or can be implicits.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14296 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26Same Implicit Arguments rule for sumbool and sumor.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14295 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-25Coqide: fixes and clarifications concerning sentence-terminatorsletouzey
- New terminators { and } are now accepted only when followed by a blank or newline. - reorganisation of coq_lex.mll : in particular stop adding a fake " " when parsing a string. - fix the handling of copy-pasted string containing tags : we isolate this zone, untag it, and retag it properly. For that we don't monitor the "changed" event anymore, but wait for a "end_user_input" instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14294 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-22Add a syntax entry for fully applied constructor patternpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14292 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-22Internalization of pattern carries a full intern_envpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14291 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-22Allow custom targets without commands specifiedpboutill
$ coq_makefile -custom "" "install2" "install" for instance does: install: install2 If you tried to do this before, coq_makefile used to insert a TAB after the rule. Signed-off-by: Paolo Herms <paolo.herms@cea.fr> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14290 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-22For the beauty of tail recursion, a new list_addnpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14289 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-20Fix typo in coqmktop helpglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14288 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-18Fixed a "feature" of "inversion" and "dependent rewrite" revealed byherbelin
the extension of "dependent rewrite" to "sig" type in r14279: in case of an equality "existT a p = x", no rewriting was done at all instead of substituting "x" as "inversion" normally does when an equality "x = t" is generated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14287 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16This adds two option tables 'Printing Record' and 'Printing Constructor'herbelin
that forces a given type to always be printed as a record, or with a constructor, regardless of the setting of 'Printing Records'. And this is that patch that controls printing by type. (patch from Tom Prince) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14286 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16This is exactly the structure needed to handle controlling printingherbelin
of terms of record type with record or constructor syntax. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14285 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
when printing. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14284 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16Some facts about functional extensionality (especially alternativeherbelin
formulations). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14283 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16More lemmas relating the different equivalent formulations of eq_dep.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14282 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14281 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16Changed name of internally defined "_sym" scheme to avoid confusion with ↵herbelin
Logic.eq_sym that has specific implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14280 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> ↵herbelin
and <- when a variable is about to be substituted (subst_one rewrite the whole context at once, while multi_rewrite rewrites each hyp independently, what may break typing in case of dependencies). Also generalize "dependent rewrite" to "sig" (to be done: generalize it to eq_dep, eq_dep1, and any dependent tuple). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14279 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16Finally, pr_goal seems to work for printing v8.2 style goal in debugger.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14278 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16Added a characterization of unique existence.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14277 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-15A correct error message for an unknown field in a record definitionpboutill
fix bug 2571. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14276 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-11Makefiles generated by coq_makefile can build %.cmx?a from %.mllibpboutill
A problem remains with the "install" rule because every cmo/cmx is installed even if installing only the generated cma/cmxa could be sufficient. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14275 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-11Stores bullet stack on locally at the level of focuses rather than globally ↵aspiwack
in the proof. Fixes bug #2568 ( http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2568 ) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14274 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-08Coqide: undo comments (Second part of r14268)pboutill
If a comment is a sentence not sent to coq, undoing a comment mustn't undo anything ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14273 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07coq_makefile logical path ending with '.' are correctly convert to physical pathpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14272 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07coq_makefile bug fix 2405: cmxs are now made from cmx filespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14271 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07coq_makefile documentation in Refman and -hpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14270 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07coq_makefile doesn't complain anymore when a dir is both -I and -Rpboutill
It used to deal correctly with that so why a warning ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14269 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07Bug 2217: In coqide, a comment alone is now a sentence that isn't send to coqpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14268 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07Coqide understand { and }pboutill
It doesn't use them for indenting. Worst, the undo around "End ..." bug leaks on '}' ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14267 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07default install location under cygwin is the unix defaultpboutill
apply patch of bug 668. At last... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14266 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07bug 2423: consider "" as the empty prefixbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14265 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07fixed coqchk usage and man page + added option -coqlibbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14264 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-06Fixed bullets so that they would play well with { }.aspiwack
We can now have script like assert P. { destruct n. - solve_case1. - solve_case2. } solve_goal However there is an undesirable interaction with Focus (which we might, anyway, consider deprecated in favour of {}). Indeed, for compatibility with v8.3, Unfocus is called implicitely after each proof command if there is no focused goal. And the new behaviour of bullets is to allow arbitrary unfocusing command "pass trough" them. As a result, a script like Focus. split - solves_first_goal will result in a fully unfocused proof. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14262 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-31 19:29:03 +0000