| Age | Commit message (Collapse) | Author |
|---|
|
"f atomic_tac" as a short-hand for "f ltac:(atomic_tac)" for "f" an
Ltac function - see Tacinterp.add_primitive_tactic).
More precisely, when parsing "f ref" and "ref" is recognized as the
name of some TACTIC-EXTEND-defined tactic parsable as an atomic tactic
(like "eauto", "firstorder", "discriminate", ...), the code was
correct only when a rule of the form `TACTIC EXTEND ... [ "foo" -> ...] END'
was given (where "foo" has no arguments in the rule) but not when a rule
of the form `TACTIC EXTEND ... [ "foo" tactic_opt(p) -> ...] END' was given
(where "foo" had an optional argument in the rule). In particular,
"firstorder" was in this case.
More generally, if, for an extra argument able to parse the empty string, a rule
`TACTIC EXTEND ... [ "foo" my_special_extra_arg(p) -> ...] END' was given,
then "foo" was not recognized as parseable as an atomic string (this
happened e.g. for "eauto"). This is now also fixed.
There was also another bug when the internal name of tactic was not
the same as the user-level name of the tactic. This is the reason why
"congruence" was not recognized when given as argument of an ltac (its
internal name is "cc").
Incidentally removed the redundant last line in the parsing rule for
"firstorder".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15041 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
did not handle let-ins and was wrongly specified). Thanks to Pierre
Boutillier and Pierre-Marie Pédrot for pointing out the source of the
bug.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This reverts commit 28bcf05dd876beea8697f6ee47ebf916a8b94cdf.
An other wrong externalize function
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15021 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dependent induction if they
don't look really trivial. We still are making a choice though. Fixes bug #2712.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14988 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14977 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14954 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
#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
|
|
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
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14903 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
|
|
with evars under binders.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14873 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14827 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14826 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
interpretation order of scoped notations).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14819 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
instantiating them in the unification algorithm used for tactics.
This allows to discard ill-typed uses of first-order unification which
otherwise would have been fatal (this incidentally allows to partially
restore some compatibility with 8.3 that was broken after eta was
added in unification).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14812 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14810 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
that used it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14802 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14800 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
printing notations. Since notation printing is not typed, printing "F G"
using a notation for "f (fun x => g)" recursively eta-expands G, then
x, then a new x and so on forever.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14796 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
New vernacular "Proof using idlist" to declare the variables
to be discharged at the end of the current proof. The system
checks that the set of declared variables is a superset of
the set of actually used variables.
It can be combined in a single line with "Proof with":
Proof with .. using ..
Proof using .. with ..
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(the number of entries to reset was not correct).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14778 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14777 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
is imported): in case of nested modules, activation was done as soon
as the outermost module was imported.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14775 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Implicit arguments can be mentioned anonymously:
Arguments map {_ _} f l.
- To rename implicit arguments, the ": rename" flag must be used:
Arguments map {T1 T2} f l : rename.
Without the ": rename" flag arguments can be used to assert
that a function has indeed the expected number of arguments and
that the arguments are named as expected.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14766 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14759 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Fixing output tests after having added flushing of warning in
revisions 14747 and 14750.
Moving Implicit output test to new command Arguments.
Adding test of new Arguments syntax in PrintInfos.v.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14758 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
pattern-unification test. They were tolerated up to r14539. Also
expanded the let-ins not bound to rel or var in the right-hand side of
a term for which pattern-unification is tested (this expansion can
refer to a non-let variable that has to be taken into account in the
pattern-unification test).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14757 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14749 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The MLcase has notably changed:
- No more case_info in it, but only a type annotation
- No more "one branch for one constructor", but rather a sequence
of patterns. Earlier "full" pattern correspond to pattern Pusual.
Patterns Pwild and Prel allow to encode optimized matchs without
hacks as earlier. Other pattern situations aren't used (yet)
by extraction, but only by P.N Tollitte's code.
A MLtuple constructor has been introduced. It isn't used by
the extraction for the moment, but only but P.N. Tollitte's code.
Many pretty-print functions in ocaml.ml and other have been reorganized
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14734 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(bug was introduced in r14703 when postprocessing started to traverse
inner cases).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14732 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Example:
Arguments eq_refl {B y}, [B] y.
Check (eq_refl (B := nat)).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14719 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The new vernacular "Arguments" attaches to constants the extra-logical
piece of information regarding implicit arguments, notation scopes and
the behaviour of the simpl tactic. The About vernacular is extended to
print the new extra logical data for simpl.
Examples:
Arguments foo {A B}%type f [T] x.
(* declares A B and T as implicit arguments, A B maximally inserted.
declares type_scope on A and B *)
Arguments foo {A%type b%nat} p%myscope q.
(* declares A and b as maximally inserted implicit arguments.
declares type_scope on A, nat_scope on b and the scope delimited by
myscope on p *)
Arguments foo (A B)%type c d.
(* declares A and b in type_scope, but not as implicit arguments. *)
Arguments foo A B c.
(* leaves implicit arguments and scopes declared for foo untouched *)
Arguments foo A B c : clear implicits
(* equivalente too Implicit Arguments foo [] *)
Arguments foo A B c : clear scopes
(* equivalente too Arguments Scope foo [_ _ _] *)
Arguments foo A B c : clear scopes, clear implicits
Arguments foo A B c : clear implicits, clear scopes
Arguments foo A B c : clear scopes and implicits
Arguments foo A B c : clear implicits and scopes
(* equivalente too Arguments Scope foo [_ _ _]. Implcit Arguments foo [] *)
Arguments foo A B c : default implicits.
(* equivalent to Implicit Arguments foo. *)
Arguments foo {A B} x , A [B] x.
(* equivalent to Implicit Arguments foo [[A] [B]] [B]. *)
Arguments foo a !b c !d.
(* foo is unfolded by simpl if b and d evaluate to a constructor *)
Arguments foo a b c / d.
(* foo is unfolded by simpl if applied to 3 arguments *)
Arguments foo a !b c / d.
(* foo is unfolded by simpl if applied to 3 arguments and if b
evaluates to a constructor *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14717 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The problem that this patch tries to solve is that sometimes the
unfolding behaviour of simpl is too aggressive, frequently exposing
match constructs. Moreover one may want some constants to never be
unfolded by simpl (like in the Math-Comp library where the nosimpl hack
is pervasive). Finally, one may want some constants to be volatile,
always unfolded by simple when applied to enough arguments, even if they
do not hide a fixpoint or a match.
A new vernacular command to be indroduced in a following patch attaches
to constants an extra-logical piece of information. It declares wich
arguments must be checked to evaluate to a constructor before performing
the unfolding of the constant (in the same spirit simpl considers as
such the recursive argument of an inner fixpoint).
Examples:
Arguments minus !x !y.
(* x and y must evaluate to a constructor for simpl to unfold minus *)
(S x - y) --- simpl ---> (S x - y)
(S x - S y) --- simpl ---> (x - y)
Definition fcomp A B C (f : B -> C) (g : A -> B) x := f (g x).
Arguments fcomp A B C f g x /.
Infix "\o" := fcomp (at level 50, left associativity) : nat_scope.
(* fcomp hides no fix, but simpl will unfold if applied to 6 arguments *)
(fun x => (f \o g) x) = f \o g --- simpl ---> (fun x => f (g x)) = f \o g
Arguments minus x y : simpl never.
(* simpl will never unfold minus *)
(S x - S y) --- simpl ---> (S x - S y)
Definition nid (x : nat) := x.
Arguments nid / x.
(* nid is volatile, unfolded by simpl when applied to 0 or more arguments *)
nid --- simpl ---> (fun x => x)
Arguments minus x y : simpl nomatch.
(* triggers for minus the "new" simpl heuristic I discussed with Hugo:
if reducing the fix would leave a match in "head" position
then don't unfold
a suggestion for a better name (for "nomatch") would be appreciated *)
(0 - y) --- simpl ---> 0
(S x - y) --- simpl ---> (S x - y)
(S x - S y) --- simpl ---> (x - y)
(minus 0) --- simpl ---> (minus 0)
(* This last test does not work as one may expect, i.e.
(minus 0) --- simpl ---> (fun _ => 0)
The point is that simpl is implemented as "strong whd_simpl"
and after unfolding minus you have
(fun m => match 0 => 0 | S n' => ...n' - m'... end)
that is already in whd and exposes a match, that of course "strong"
would reduce away but at that stage we don't know, and reducing by
hand under the lambda is against whd reduction. So further discussion
on that idea is needed. *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14716 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
to the dependencies in the real arguments (a.k.a. indices) of the
terms to match.
This allows in particular to make the example from bug report #2404
work.
TODO: move the computation of dependencies in compile_branch at the time
of splitting a branch (where the computation is done now, it does not allow
to support dependent matching on the second argument of a constructor of
type "forall b, (if b then Vector.t n else nat) -> Vector.t n -> foo").
TODO: take dependencies in Var's into account and take dependencies within
non-Rel arguments also into account (as in "match v (f t) with ... end"
where v is a Var and the type of (f t) depends on it).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14711 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14705 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14703 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
main criterion is to look at whether the alias to the term to match is
dependent in the return predicate or not. Since the exact return
predicate is often found late, the detection is done after the
subproblem is fully compiled, when a maximum amount of (local)
information on typing is known.
Eventually, we should go to a model where all possible partial
expansions of an alias are usable at typing time. Indeed the current
heuristic (like the previous one) is not fully safe since it might
decide not to expand an alias in a branch whose type does not depend
of the alias but the typing of the branch internally needs the
expansion (as e.g. in "fun (H:forall n, n=0->Prop) n => match n with 0
as x => H x eq_refl | _ => True end").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14701 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14700 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
how the names of an ltac expression are globalized - allowing the
expression to be a constr and in some initial context - and when and
how this ltac expression is interpreted - now expecting a pure tactic
in a different context).
This incidentally found a Ltac bug in Ncring_polynom!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14676 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14674 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(technically, since the signature "tomatch" of terms to match and of
terms to generalize is typed in a context that does not consider terms
to match as binders while the return predicate do consider them as
binders, the adjusment of the context of the "tomatch" to the context
of the predicate needs lifting in each missing part of the "tomatch"
context, what was not done)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14664 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14658 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The check looks for 1 canonical projection applied to a meta/evar.
This fails to deal with telescopes that generate unification problems
containing something like "(pi_1 (pi_2 ?))" that is indeed a "stuck"
canonical projection but not of the form recognized by the previous
implementation. The same holds when pi_2 is a general function not
producing a constructor.
This patch checks if the argument of the canonical projection weak head
reduces to a constructor calling whd_betadeltaiota.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14645 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
For instance, consider this inductive type:
Inductive Ind := A | B | C | D.
For detecting "match" on this type, one was forced earlier to write code
in Ltac using "match goal" and/or "context [...]" and long patterns such as:
match _ with A => _ | B => _ | C => _ | D => _ end
After this patch, this pattern can be shortened in many alternative ways:
match _ with A => _ | _ => _ end
match _ with B => _ | _ => _ end
match _ in Ind with _ => _ end
Indeed, if we want to detect a "match" of a given type, we can either
leave at least one branch where a constructor is explicit, or use a "in"
annotation.
Now, we can also detect any "match" regardless of its type:
match _ with _ => _ end
Note : this will even detect "match" over empty inductive types.
Compatibility should be preserved, since "match _ with end" will
continue to correspond only to empty inductive types.
Internally, the constr_pattern PCase has changed quite a lot, a few elements
are now grouped into a case_info_pattern record, while branches are now
lists of given sub-patterns.
NB: writing "match" with missing last branches in a constr pattern was actually
tolerated by Pattern.pattern_of_glob_constr earlier, since the number of
constructor per inductive is unknown there. And this was triggering an uncaught
exception in a array_fold_left_2 in Matching later. Oups. At least this patch
fixes this issue...
Btw: the code in Pattern.pattern_of_glob_constr was quadratic in the number
of branch in a match pattern. I doubt this was really a problem, but having now
linear code instead cannot harm ;-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14644 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in r14199 (June 2011). Meta's implicitly depend on the context they are
defined in and this has to be taken into account for checking if
occurrences are distinct (in particular, no Var's are allowed as
arguments of a pattern-unifiable Meta). The example expected to be
accepted thanks to r14199 is not a pattern-unification problem (it has
more than one solution) and was anyway already accepted (strange).
Compared to before r14199, aliases expansion and restriction of
pattern unification check to variables occurring in the right-hand
side are however now taken into account.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14642 85f007b7-540e-0410-9357-904b9bb8a0f7
|
