aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* Set Extraction KeepSingleton: an option for not decapsulating singleton typesGravatar letouzey2011-07-04
| | | | | | | | | | | | 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
* StrictOrder marked explicitly to be in PropGravatar letouzey2011-07-04
| | | | | | | 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
* Extraction: in haskell, __ may have any type, no need to unsafeCoerce itGravatar letouzey2011-07-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14258 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552)Gravatar letouzey2011-07-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14257 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: forbid Prop-polymorphism of inductives when extracting to OcamlGravatar letouzey2011-07-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* doc/stdlib: Update the list of ZArith filesGravatar letouzey2011-07-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14255 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some cleanup of ZcomplementsGravatar letouzey2011-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14254 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup of files related with power over Z.Gravatar letouzey2011-07-01
| | | | | | | | | | | | | | - 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
* Fix compilation errorGravatar msozeau2011-06-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14252 85f007b7-540e-0410-9357-904b9bb8a0f7
* Keep obligation source information in ProgramGravatar msozeau2011-06-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14251 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup in SpecViaZGravatar letouzey2011-06-30
| | | | | | | | | 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
* Cleanup of NdigitsGravatar letouzey2011-06-30
| | | | | | | | | | - 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
* update of Micromega docGravatar fbesson2011-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14248 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deletion of useless Zdigits_defGravatar letouzey2011-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14247 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deletion of useless Zlog_defGravatar letouzey2011-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14246 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deletion of useless Zsqrt_defGravatar letouzey2011-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_defGravatar letouzey2011-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14244 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some cleanup of Wf_Z.vGravatar letouzey2011-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14243 85f007b7-540e-0410-9357-904b9bb8a0f7
* improved tactic namesGravatar fbesson2011-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14242 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some more cleanups (Zeven, auxiliary, Zbool, Zmisc, ZArith_base)Gravatar letouzey2011-06-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14241 85f007b7-540e-0410-9357-904b9bb8a0f7
* Znumtheory: a correct version of a compatibility Zdivide_introGravatar letouzey2011-06-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14240 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clean-up of Znumtheory, deletion of Zgcd_defGravatar letouzey2011-06-24
| | | | | | | | | | | In particular, we merge the old Zdivide (used to be an ad-hoc inductive predicate) and the new Z.divide (based on exists). Notations allow to do that (almost) transparently, the only impact is that the name picked by the system will not be "q" anymore when destructing a Z.divide. Some fragile scripts may have to be fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14239 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: a particular case of div_uniqueGravatar letouzey2011-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14238 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: change definition of divide (compat with Znumtheory)Gravatar letouzey2011-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14237 85f007b7-540e-0410-9357-904b9bb8a0f7
* cleanup of ZsgnGravatar letouzey2011-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14236 85f007b7-540e-0410-9357-904b9bb8a0f7
* cleanup of Zmin and ZmaxGravatar letouzey2011-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14235 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some more cleanup of ZorderGravatar letouzey2011-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14234 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 13:53:32 +0000