aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-01-31Fix camlp4 compilationpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14951 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-30Added an pattern / occurence syntax for vm_compute.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14950 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-28Tentative to fix bug #2628 by not letting intuition break records. Might be ↵msozeau
too much of a backwards-incompatible change git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14949 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-28Fix simplification of ind. hyps., recognized by a [block] in their type (bug ↵msozeau
#2674) and properly clear [block] at end of simplification (bug #2691). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14948 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-27Printing bugs with match patterns:herbelin
- namegen.ml: if a matching variable has the same name as a constructor, rename it, even if the conflicting constructor name is defined in a different module; - constrextern.ml: protect code for printing cases as terms are from requesting info in the global env when printers are called from ocamldebug since the global env is undefined in this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14947 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-26Fail: discard the effects of a successful command (fix #2682)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14945 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-26Add support for plugin initialization functiongareuselesinge
Plugins can call add_known_plugin instead of add_known_module to specify an initialization function. That function is granted to be called after the system initialization (in case of static linking) and every time their are "loaded" with Declare ML Module (even if the .cmo or .cmxs is actually loaded only once since OCaml is unable to unload dynamically linked modules). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14944 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-25Check for unresolved evars in textual order of the params and fields ↵msozeau
declarations (fixes bug #2278). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14943 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-23Fix bug #2483: anomaly raised due to wrong handling of the evars state.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14942 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-23Fix typeclass resolution error message which included goal evars (bug #2620).msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14941 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-23Fix for Program Instance not separately checking the resolution of evars of ↵msozeau
the type (mandatory) and the fields (optional) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14940 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-23Another quick hack that works this time, to handle printing of locality in ↵ppedrot
Program subtac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14939 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-23Deleted the only use of BeginSubProof from the standard library.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14938 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 17:15:18 +0000