aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-01-17Makefile: fix make distclean w.r.t. test-suiteletouzey
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
2012-01-17MSetAVL: better implementation of filter suggested by X. Leroyletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14914 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-17Some fix in beautify pretty-printerpboutill
- 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
2012-01-16Parameters in pattern first step.pboutill
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
2012-01-16Inductiveops.nb_*{,_env} cleaningpboutill
- 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
2012-01-16Bug 2679: Do not try to install cmxs with -byte-onlypboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14907 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-16Bug 2676: ./configure --prefix shoudn't ask for a config directory.pboutill
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
2012-01-16make mli-doc fixpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14905 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-14coq_micromega.ml: fix order of recursive calls to rconstantglondu
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
2012-01-14Add distclean back to test-suite/Makefileglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14903 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-14More newlines in debugging output of psatzlglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14902 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-13Added a Btauto plugin, that solves boolean tautologies.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14897 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-13Added the decidability of (<=) on nat.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14896 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-12Fix typoglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14893 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-10Fix printing of instances, generalized arguments.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14892 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-07Fix typoglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14889 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-06Fixed the itarget of the previous commit...ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14888 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-06Added a typeclass-based system to reason on decidable propositions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14887 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-06Forbids (as it has always been the behaviour) to have two different openaspiwack
proofs with the same name. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14884 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-06Fixes bug #2654 (tactic instantiate failing to update existential variables).aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14883 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-05Backtracking on r14876 (fix for bug #2267): extra scopes might beherbelin
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
2012-01-04Fixing Arguments Scope bug when too many scopes are given (bug #2667).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14876 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-04Type inference unification: fixed a 8.4 bug in the presence of unificationherbelin
with evars under binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14873 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-03Makefile.doc: attempt to solve race condition for creating doc/refman/html.herbelin
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
2011-12-27Bug 2669 and more: make full-stdlibpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14869 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-26Coqdoc: Fixing missing newline when using "Proof term."herbelin
(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
2011-12-26Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14864 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-26update CHANGES w.r.t. simplgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14863 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-25Version number, copyright, credits: missing updates.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14862 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-23Credits for 8.4: More exhaustive list of external contributors.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14852 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-23myocamlbuild: -DWIN32 instead of -DWin32letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14849 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-23Configure: the backslashes in win32 paths should be escapedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14848 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-22Credits for 8.4 + resetting COMPATIBILITY file.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14846 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-21sequel of previous commitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14842 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-21Isolate a few types of Goptions in a pure .mli, solving a dep issue with ↵letouzey
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
2011-12-21Pure interfaces shouldn't be mentionned in .mllibletouzey
.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
2011-12-21adapt myocamlbuild after changes in coqdep_boot (.beautify)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14839 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-21Cleaning CHANGES file.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14837 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-19Notifying removal of accidental unfolding of recursive calls ofherbelin
fixpoints by destruct/inversion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14828 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-19Arguments: check rename even if no implicit is specifiedgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14827 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-19test suite update after r14808pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14826 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-19Bug 2377 part 2: old revision file is erased by installpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14825 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-19Fixed some printing details for dependent evars in emacs mode. Patchcourtieu
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
2011-12-18Granted legitimate wish #2607 (not exposing crude fixpoint body ofherbelin
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
2011-12-18CoqIde files position is freedesktop compliant.pboutill
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
2011-12-18./configure & freedesktoppboutill
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
2011-12-18Fixing bug #2634 (unscoped notations were disturbing theherbelin
interpretation order of scoped notations). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14819 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18Applied patches proposed suggested by Hendrik Tews to fix existentialcourtieu
variables printing in emacs mode (put them at the end of input, and fix commas). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14818 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18Continuing 14812 and 14813 (use type information to reduce theherbelin
applicability of first-order unification in tactic unification). Don't try to unify the type (this would require a unification power that unification.ml does not have - and some contribs complain about that). Just reject first-order unification of metavariables of higher-order types when their types are obviously incompatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14817 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18Fixed a Not_found bug when declaring in a section some implicitherbelin
arguments for a constant not defined in the section. Also fixed some typos in the doc of implicit arguments in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14816 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:56:29 +0000