aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Pretty printing of generalized binderGravatar pboutill2012-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Boolean Option Patterns CompatibilityGravatar pboutill2012-01-19
| | | | | | | switch between "all arguments no parameters" and "explicit params and args" for constructor arguments in patterns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14919 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more use of tauto in Init/Gravatar pboutill2012-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14918 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed the pretty-printing of the Program plugin.Gravatar ppedrot2012-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: fix make distclean w.r.t. test-suiteGravatar letouzey2012-01-17
| | | | | | | | No need for a distclean rule in test-suite, since the root-level distclean already launches clean, which launches clean in test-suite, and this one does the job git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14915 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetAVL: better implementation of filter suggested by X. LeroyGravatar letouzey2012-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14914 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some fix in beautify pretty-printerGravatar pboutill2012-01-17
| | | | | | | | | - In binders, {X} were printed X - Notation toto x y := were printed Notation totox y - Fixpoint declaration prints too much spaces Hunt is not closed yet anyway... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14913 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parameters in pattern first step.Gravatar pboutill2012-01-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In interp/constrintern.ml, '_' for constructor parameter are required if you use AppExpl ('@Constr') and added in order to be erased at the last time if you do not use '@'. It makes the use of notation in pattern more permissive. For example, -8<------ Inductive I (A: Type) : Type := C : A -> I A. Notation "x <: T" := (C T x) (at level 38). Definition uncast A (x : I A) := match x with | x <: _ => x end. -8<------ was forbidden. Backward compatibility is strictly preserved expect for syntactic definitions: While defining "Notation SOME = @Some", SOME had a special treatment and used to be an alias of Some in pattern. It is now uniformly an alias of @Some ('_' must be provided for parameters). In interp/constrextern.ml, except if all the parameters are implicit and all the arguments explicit (This covers all the cases of the test-suite), pattern are generated with AppExpl (id est '@') (so with '_' for parameters) in order to become compatible in any case with future behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14909 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductiveops.nb_*{,_env} cleaningGravatar pboutill2012-01-16
| | | | | | | - Functions without _env use the global env. - More comments about when letin are counted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14908 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2679: Do not try to install cmxs with -byte-onlyGravatar pboutill2012-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14907 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2676: ./configure --prefix shoudn't ask for a config directory.Gravatar pboutill2012-01-16
| | | | | | I am not really happy of /etc/xdg/coq ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14906 85f007b7-540e-0410-9357-904b9bb8a0f7
* make mli-doc fixGravatar pboutill2012-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14905 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_micromega.ml: fix order of recursive calls to rconstantGravatar glondu2012-01-14
| | | | | | | | Some tests were failing on architectures without native code because the evaluation order of arguments in a function call is not the same on bytecode, leading to different behaviours for the psatzl tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14904 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add distclean back to test-suite/MakefileGravatar glondu2012-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14903 85f007b7-540e-0410-9357-904b9bb8a0f7
* More newlines in debugging output of psatzlGravatar glondu2012-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14902 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a Btauto plugin, that solves boolean tautologies.Gravatar ppedrot2012-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14897 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added the decidability of (<=) on nat.Gravatar ppedrot2012-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14896 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typoGravatar glondu2012-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14893 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix printing of instances, generalized arguments.Gravatar msozeau2012-01-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typoGravatar glondu2012-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed the itarget of the previous commit...Gravatar ppedrot2012-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14888 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a typeclass-based system to reason on decidable propositions.Gravatar ppedrot2012-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14887 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forbids (as it has always been the behaviour) to have two different openGravatar aspiwack2012-01-06
| | | | | | proofs with the same name. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14884 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes bug #2654 (tactic instantiate failing to update existential variables).Gravatar aspiwack2012-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14883 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtracking on r14876 (fix for bug #2267): extra scopes might beGravatar herbelin2012-01-05
| | | | | | | useful in the presence of coercions to Funclass. Fixed the bug differently. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14880 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Arguments Scope bug when too many scopes are given (bug #2667).Gravatar herbelin2012-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Type inference unification: fixed a 8.4 bug in the presence of unificationGravatar herbelin2012-01-04
| | | | | | with evars under binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14873 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.doc: attempt to solve race condition for creating doc/refman/html.Gravatar herbelin2012-01-03
| | | | | | | | | Indeed, $INDEXURLS requires files from $INDEXES to be built and all of these files plus target doc/refman/html/index.html ask in parallel to erase and rebuild the doc/refman/html. Tried to use an intermediate phony target to factorize the rebuilding of doc/refman/html. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14872 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2669 and more: make full-stdlibGravatar pboutill2011-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14869 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdoc: Fixing missing newline when using "Proof term."Gravatar herbelin2011-12-26
| | | | | | | (bug apparently introduced by r11880). Fixing also a "body_bol" which apparently should be a "bol". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14866 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).Gravatar herbelin2011-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14864 85f007b7-540e-0410-9357-904b9bb8a0f7
* update CHANGES w.r.t. simplGravatar gareuselesinge2011-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14863 85f007b7-540e-0410-9357-904b9bb8a0f7
* Version number, copyright, credits: missing updates.Gravatar herbelin2011-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14862 85f007b7-540e-0410-9357-904b9bb8a0f7
* Credits for 8.4: More exhaustive list of external contributors.Gravatar herbelin2011-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14852 85f007b7-540e-0410-9357-904b9bb8a0f7
* myocamlbuild: -DWIN32 instead of -DWin32Gravatar letouzey2011-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14849 85f007b7-540e-0410-9357-904b9bb8a0f7
* Configure: the backslashes in win32 paths should be escapedGravatar letouzey2011-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14848 85f007b7-540e-0410-9357-904b9bb8a0f7
* Credits for 8.4 + resetting COMPATIBILITY file.Gravatar herbelin2011-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14846 85f007b7-540e-0410-9357-904b9bb8a0f7
* sequel of previous commitGravatar letouzey2011-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Isolate a few types of Goptions in a pure .mli, solving a dep issue with ↵Gravatar letouzey2011-12-21
| | | | | | | | | | | | | | ocamlbuild A few types of Goptions are mentioned in toplevel/interface.mli. Since the latter is a pure .mli, this shouldn't trigger a dependency with respect to goptions.ml, but apparently ocamlbuild isn't clever enough to notice this, and hence wants to link a pile of useless stuff with coqide. I'll discuss with Pierre-Marie about the best long-term way to avoid this mess, but in the meantime I split the concerned types of Goptions in a separate Goptionstyp.mli. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14841 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pure interfaces shouldn't be mentionned in .mllibGravatar letouzey2011-12-21
| | | | | | | | | | | .mllib should only mention *code* to be linked in .cma and later executable, but not .mli without .ml. Otherwise, really nasty errors occur with ocamlbuild, for instance some rules appears to be ignored and masked by default ones, etc etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14840 85f007b7-540e-0410-9357-904b9bb8a0f7
* adapt myocamlbuild after changes in coqdep_boot (.beautify)Gravatar letouzey2011-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14839 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning CHANGES file.Gravatar herbelin2011-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14837 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notifying removal of accidental unfolding of recursive calls ofGravatar herbelin2011-12-19
| | | | | | fixpoints by destruct/inversion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14828 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arguments: check rename even if no implicit is specifiedGravatar gareuselesinge2011-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14827 85f007b7-540e-0410-9357-904b9bb8a0f7
* test suite update after r14808Gravatar pboutill2011-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14826 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2377 part 2: old revision file is erased by installGravatar pboutill2011-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14825 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed some printing details for dependent evars in emacs mode. PatchGravatar courtieu2011-12-19
| | | | | | | | | | | | | | | | from Hendrik Tews: 1) Print the dependent evars after "No more subgoals" and after "No more subgoals but non-instantiated existential". This is necessary to correctly display the instantiation status of dependent evars, because the last proof command might change them. 2) Change the ``Show Goal "id"'' command to include a header like goal / evar 2 is: This is more consistent with the other Show commands. Moreover it simplifies the use of this command in Proof General, because, with the change, the output contains the goal ID. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14824 85f007b7-540e-0410-9357-904b9bb8a0f7
* Granted legitimate wish #2607 (not exposing crude fixpoint body ofGravatar herbelin2011-12-18
| | | | | | | unfolded fixpoints when calling destruct). However, this might break compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14823 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIde files position is freedesktop compliant.Gravatar pboutill2011-12-18
| | | | | | | Beware, it means that files position is not relative to coqtop position but is given by XDG_DATA_DIRS and XDG_CONFIG_DIRS. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14822 85f007b7-540e-0410-9357-904b9bb8a0f7
* ./configure & freedesktopGravatar pboutill2011-12-18
| | | | | | | | 1/ man dir is now prefix/share/man and not prefix/man git diff! 2/ a data dir option for coqide extra data. 3/ typo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14821 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 17:34:10 +0000