aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Hipattern: two generic equalities on constr spotted & rewrittenGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Indtypes: remove useless and wrong generic equality test on constr arrayGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14315 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: slight reorganization of the fileGravatar puech2011-07-29
| | | | | | | - 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
* Term_typing, Typeops: replace some generic '=' on constr by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14313 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: Refactoring of hashconsingGravatar puech2011-07-29
| | | | | | | - 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
* argument renaming in liftn (match with usual terminology)Gravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14311 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide_slave: same attributes for { } and Focus/Unfocus (fix coqide display)Gravatar letouzey2011-07-28
| | | | | | | 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
* Coqide: GEdit.combo is deprecated since Gtk2.4! We now use ↵Gravatar pboutill2011-07-27
| | | | | | GEdit.combo_box_entry_text git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14306 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oversight in revision 14292.Gravatar pboutill2011-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14305 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo of bug 2577Gravatar pboutill2011-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14303 85f007b7-540e-0410-9357-904b9bb8a0f7
* or_introl is now too complicated for basic tests of ↵Gravatar pboutill2011-07-26
| | | | | | | | | 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
* Partial revert of r14292Gravatar pboutill2011-07-26
| | | | | | 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
* ide/coq_lex.mll: restore the separate parsing of .. (fix #2578)Gravatar letouzey2011-07-26
| | | | | | | | | | | | | | | | 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
* Integral domainsGravatar pottier2011-07-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14299 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ring2 devient Ncring et la reification par les type classes est partageeGravatar pottier2011-07-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14298 85f007b7-540e-0410-9357-904b9bb8a0f7
* All the parameters of Compare are implicits.Gravatar pboutill2011-07-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14297 85f007b7-540e-0410-9357-904b9bb8a0f7
* All the parameters of or can be implicits.Gravatar pboutill2011-07-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14296 85f007b7-540e-0410-9357-904b9bb8a0f7
* Same Implicit Arguments rule for sumbool and sumor.Gravatar pboutill2011-07-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: fixes and clarifications concerning sentence-terminatorsGravatar letouzey2011-07-25
| | | | | | | | | | | | | | | - 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
* Add a syntax entry for fully applied constructor patternGravatar pboutill2011-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14292 85f007b7-540e-0410-9357-904b9bb8a0f7
* Internalization of pattern carries a full intern_envGravatar pboutill2011-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14291 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow custom targets without commands specifiedGravatar pboutill2011-07-22
| | | | | | | | | | | | | | $ 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
* For the beauty of tail recursion, a new list_addnGravatar pboutill2011-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14289 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typo in coqmktop helpGravatar glondu2011-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14288 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a "feature" of "inversion" and "dependent rewrite" revealed byGravatar herbelin2011-07-18
| | | | | | | | | 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
* This adds two option tables 'Printing Record' and 'Printing Constructor'Gravatar herbelin2011-07-16
| | | | | | | | | | | 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
* This is exactly the structure needed to handle controlling printingGravatar herbelin2011-07-16
| | | | | | | | 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
* This option disables the use of the '{| field := ... |}' notationGravatar herbelin2011-07-16
| | | | | | | | 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
* Some facts about functional extensionality (especially alternativeGravatar herbelin2011-07-16
| | | | | | formulations). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14283 85f007b7-540e-0410-9357-904b9bb8a0f7
* More lemmas relating the different equivalent formulations of eq_dep.Gravatar herbelin2011-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14282 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)Gravatar herbelin2011-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14281 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changed name of internally defined "_sym" scheme to avoid confusion with ↵Gravatar herbelin2011-07-16
| | | | | | 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
* Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> ↵Gravatar herbelin2011-07-16
| | | | | | 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
* Finally, pr_goal seems to work for printing v8.2 style goal in debugger.Gravatar herbelin2011-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14278 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a characterization of unique existence.Gravatar herbelin2011-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14277 85f007b7-540e-0410-9357-904b9bb8a0f7
* A correct error message for an unknown field in a record definitionGravatar pboutill2011-07-15
| | | | | | fix bug 2571. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14276 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefiles generated by coq_makefile can build %.cmx?a from %.mllibGravatar pboutill2011-07-11
| | | | | | | 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
* Stores bullet stack on locally at the level of focuses rather than globally ↵Gravatar aspiwack2011-07-11
| | | | | | | | 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
* Coqide: undo comments (Second part of r14268)Gravatar pboutill2011-07-08
| | | | | | | 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
* coq_makefile logical path ending with '.' are correctly convert to physical pathGravatar pboutill2011-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14272 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_makefile bug fix 2405: cmxs are now made from cmx filesGravatar pboutill2011-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14271 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_makefile documentation in Refman and -hGravatar pboutill2011-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14270 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_makefile doesn't complain anymore when a dir is both -I and -RGravatar pboutill2011-07-07
| | | | | | 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
* Bug 2217: In coqide, a comment alone is now a sentence that isn't send to coqGravatar pboutill2011-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14268 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide understand { and }Gravatar pboutill2011-07-07
| | | | | | | 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
* default install location under cygwin is the unix defaultGravatar pboutill2011-07-07
| | | | | | 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
* bug 2423: consider "" as the empty prefixGravatar barras2011-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14265 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed coqchk usage and man page + added option -coqlibGravatar barras2011-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14264 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bullets so that they would play well with { }.Gravatar aspiwack2011-07-06
| | | | | | | | | | | | | | | | | | 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
* Adding a new syntax for BeginSubproof and EndSubproof, namely { and }.Gravatar courtieu2011-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14261 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 17:01:01 +0000