aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2011-07-05Adding a new syntax for BeginSubproof and EndSubproof, namely { and }.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14261 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-04Set Extraction KeepSingleton: an option for not decapsulating singleton typesletouzey
A informative inductive type with one constructor C and one informative arg to C is normally extracted as an identity, with C removed, see for example the "sig" type. When this new option is set, these singleton types are left untouch, providing extracted code which is closer to the initial Coq development. Feature requested by Wouter Swiestra. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14260 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-04StrictOrder marked explicitly to be in Propletouzey
In fact, due to sort-polymorphism, StrictOrder was already in Prop, but it's clearer this way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14259 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-04Extraction: in haskell, __ may have any type, no need to unsafeCoerce itletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14258 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-04Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14257 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-04Extraction: forbid Prop-polymorphism of inductives when extracting to Ocamlletouzey
A particular case in sort-polymorphism of inductive types allows an informative type (such as prod) to have instances in Prop: (I,I) : True * True : Prop This is due to the fact that prod is a singleton type: indeed (I,I) has no informative content. But this invalidates an important invariant for the correctness of the extraction: inductive constructors stop having always the same sort as their inductive type. Consider for instance: Definition f (X:Type)(x:X*X)(g:X->nat) := g (fst x). Definition test := f _ (I,I) (fun _ => 0). Then the inductive element (I,I) is extracted as a logical part __, but during a strict evaluation (i.e. in Ocaml, not Haskell), this __ will be given to fst, and hence to a match, leading to a nasty result (potentially segfault). Haskell is not affected, since fst is never evaluated. This patch adds a check for this situation during any Ocaml extraction, leading for the moment to a fatal error. Some functions in inductive.ml and retyping.ml now have an extra optional argument ?(polyprop=true) that should stay untouched in regular Coq usage, while type-checking done during extraction will disable this prop-polymorphism. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14256 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-04doc/stdlib: Update the list of ZArith filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14255 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-01Some cleanup of Zcomplementsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14254 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-01Cleanup of files related with power over Z.letouzey
- Zpow_def, Zpower, Zpow_facts shortened thanks to stuff in BinInt.Z - The alternative Zpower_alt is now in a separate file Zpow_alt.v, not loaded by default. - Some more injection lemmas in Znat (pow, div, mod, quot, rem) - Btw, added a "square" function in Z, N, Pos, ... (instead of Zpow_facts.Zsquare). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14253 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-30Fix compilation errormsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14252 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-30Keep obligation source information in Programmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14251 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-30Cleanup in SpecViaZletouzey
Note that in NSig (and hence NMake and BigN), to_N is now Z.to_N (to_Z ...) instead of Z.abs_N (to_Z ...). This doesn't change the result (since to_Z create non-negative integers), but some proofs may have to be adapted git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14250 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-30Cleanup of Ndigitsletouzey
- No need for compatibility notations for stuff introduced strictly after branching of 8.3, for instance Nor, Nand, etc. - Properties for N.lor, N.lxor, etc are now in BinNat.N, no need to duplicate them in Ndigits, apart from the few compatibility results about xor. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14249 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-29update of Micromega docfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14248 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-28Deletion of useless Zdigits_defletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14247 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-28Deletion of useless Zlog_defletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14246 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-28Deletion of useless Zsqrt_defletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14245 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-28Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_defletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14244 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-28Some cleanup of Wf_Z.vletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14243 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 20:56:31 +0000