aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-01-23Removed a seemingly unused argument in Require of modules, introduced 10 ↵ppedrot
years ago and absent from both coq and contribs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14937 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-23Fixed pretty-printing of Opaque, Transparent and Strategy locality flags.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14936 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-23Bug 739: forbid dumpglob while using Coqtop in interactive modepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14935 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-21Coqtop and coqc: cleaning description of options in RefMan and manpages.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14934 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20Added documentation for "r foo" in Ltac debugger.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14931 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20Added documentation for "Set Parsing Explicit" + fixed mistakenlyherbelin
committed "assert" in commit r14928. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14930 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20Breakpoints in Ltac debugger: new command "r foo" to jump to the nextherbelin
call to "idtac foo" in Ltac code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14929 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20Added new command "Set Parsing Explicit" for deactivating parsing (andherbelin
printing) of implicit arguments (a priori useful for teaching). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14928 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20Notations with binders: Accepting using notations for functional termsherbelin
which do not necessarily depend on their parameter (e.g. a notation for "fun x => t" might match also "fun _ => t"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14926 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20Reverted previous commit, which broke library compilation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14925 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20This is a quick hack to permit the parsing of the locality flag in the ↵ppedrot
Program subtactic. Ideally, locality flags should be handled in a nicer way... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14924 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20Fix printing of classesmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14923 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-19Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14922 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-19Added the btauto tactic to the documentation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14921 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-19Pretty printing of generalized binderpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14920 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-19Boolean Option Patterns Compatibilitypboutill
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
2012-01-19No more use of tauto in Init/pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14918 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-17Fixed the pretty-printing of the Program plugin.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14917 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 17:59:12 +0000