aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2011-07-29Tactics: generic equality on named_declaration replaced by eq_named_declarationpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14320 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Term: added function eq_named_declarationpuech
We need to move eq_constr upwards git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14319 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Evarutil: generic equality on constr replaced by eq_constrpuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14318 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-25 11:48:51 +0000