| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
#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
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14945 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
declarations (fixes bug #2278).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14943 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14942 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14941 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
Program subtac.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14938 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14936 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14935 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14934 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14931 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
committed "assert" in commit r14928.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14930 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14925 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14923 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14922 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14921 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14918 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14917 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14914 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14907 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14905 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14903 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14902 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14897 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14896 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14893 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14892 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14889 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14888 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14887 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
proofs with the same name.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14884 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14883 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14876 85f007b7-540e-0410-9357-904b9bb8a0f7
|