| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15079 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Canonical Structure inference works on named terms only: i.e.
the projection and the value must be named (with few exceptions).
The set of named (head) terms is:
(Var _|Construct _|Ind _|Const _|Prod _|Sort _)
The set of unnamed is thus:
(Case _|Fix _|CoFix _|Evar _|Meta _|Rel _)
The MaybeFlex/MaybeFlex case, when no CS inference takes place,
unfolds the rhs only if it exposes a named term. If it exposes
an unnamed term, it tries to unfold on the lhs first. Note that
unnamed terms are whd normal terms, since iota and zeta are
performed by evar_apprec. So the algorithm behaves as before,
but stops unfolding the rhs 1 delta step before it exposes an
unnamed term. Then it starts unfolding the lhs. If the lhs
exposes a rigid term the rhs is naturally unfolded, going back
to same situation in which the algorithm was ending before.
But while it unfolds on the left, the rhs is still named, and
canonical structure inference can succeed.
Ex failing before, the "canon_" prefix marks projections/values
declared as canonical.
Record test := K { canon_proj : nat }
(* canon_proj x := math x with K y => y end *)
canon_val x := match x with 0 => 0 | S m => m end
Canonical Structure canon_struct x := K (canon_val x)
(* aliases *)
proj := canon_proj
val := canon_val
Old alg:
proj ? ===?=== val x
proj ? ===?=== canon_val x
proj ? ===?=== match x with ... end
canon_proj ? ===?=== match x with ... end (* no inference *)
match ? with K x...end ===?=== match x with 0 ...end (* FAIL *)
New alg:
proj ? ===?=== val x
proj ? ===?=== canon_val x
canon_proj ? ===?=== canon_val x (* inference works: ? := canon_struct *)
In case canon_struct is not declared for canon_proj and canon_val
it continues like that:
canon_proj ? ===?=== canon_val x
match ? with K x...end ===?=== canon_val x
match ? with K x...end ===?=== match x with 0 ...end (* FAIL *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15077 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15076 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It seems that we can currently do a successful Undo (but not two!)
on a freshly started Lemma. Let's add a depth check on Pfedit.undo
to avoid that. This way, we cannot Undo to depth < 1 (with 1 being
the initial depth of a lemma).
Simplier implementation of Pfedit.restart : it is Pfedit.undo_todepth 1.
This extra initial step in the Undo Stack has probably something
to see with the Lemma argument introduction. For instance, before this
patch we had:
Lemma test n : n+0=n.
Restart. (* now the goal is universally quantified ! *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15075 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
by default typeclass resolution is not launched on goal evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15074 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
i.e.: after a brace is open, one can use the bullets again without clashing with
bullets outside the brace. In particular, one can nest bullets with arbitrary
depth (by interleaving them with occasional braces).
Also fixed a typo introduced in my previous commit which caused bullets
and braces to behave just like regular focuses.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15073 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
was provoking an anomaly instead of a regular error).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15070 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The optimisation done of Namegen.visibly_occur_id did not preserve
the previous behavior when pr_constr/constr_extern/detype were
called on a term with free rel variables. We backtrack on it to
go back to the 8.2 behavior.
Seized this opportunity to clarify the meaning of the at_top flag
in constrextern.ml and printer.ml and to rename it into
goal_concl_style. The badly-named at_top flag was introduced in
Coq 6.3 in 1999 to mean that when printing variables bound in the
goal, names had to avoid the names of the variables of the goal
context, so as to keep naming stable when using "intro"; in
r4458, printing improved by not avoiding names that were short
names of global definitions, e.g. "S", or "O" (except when the
at_top flag was on for compatibility reasons).
Other printing strategies could be possible in the
non-goal-concl-style mode. For instance, all bound variables
could be made distinct in a given expression, even if no clash
occur, therefore following so-called Barendregt's
convention. This could be done by setting "avoid"
to "ids_of_rel_context (rel_context env)" in extern_constr and
extern_type (and then, Namegen.visibly_occur_id could be
re-simplified again!).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15067 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
tactic arguments of ltac functions).
Added support for recursive entries in ARGUMENT EXTEND, for right-hand
sides of ARGUMENT EXTEND raising exceptions and for right-hand sides
referring to "loc". Also fixed parsing level of initial value in
create_arg (raw instead of glob). Thanks to the Ssreflect plugin for
revealing these problems.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15065 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
solve the following kind of code broken by being less restrictive on
projecting:
Set Printing Existential Instances.
Parameter f : forall x, x=0 -> x=0 -> x=1 /\ x=2.
Parameter g : forall y, y=0 /\ y=0.
Check match g _ with conj a b => f _ a b end.
(* and the return clause should not depend on the "_" *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15064 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
try to solve remaining constraints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15063 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
candidate for the possible projection (as was introduced in 8.4beta)
but try also to imitate (as was done before 8.4beta but not done in
8.4beta).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15062 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- use evar candidates instead of postponed conversion problems when
it is known (according to the projection heuristic used) that an
evar has only a fixed number of possible instances (as e.g. in
equation ?n[x,x] = x, with x a variable);
- this allows to be more robust in solving remaining problems: if
several instanciations exist, and one is not compatible with a previous
instantiation made among several choices for another evar,
backtracking is now possible;
- this allows in particular to fix regression #2670 (two postponed
conversion problems solved in an inconsistent way);
- but this requires more code.
At the same time, a refactoring of the code has been made so as to
hopefully clarify the elementary pieces of the algorithm. For
instance, there are now generic functions for both applying a filter
and giving candidates. The filter is systematically generalized so as
to have the ccl of the evar well-typed even in situations where we
could try on the contrary to restrict the evars occurring in the
ccl.
Anyway, when the representation of instances will be optimized using
identity substitutions, it will no longer be useful to use the filter
to shorten the size of the instances. Then, the filters will have,
like candidates, the only role of restricting the search space for
potential solutions to the unification problems.
Also, solve_refl can now be used to restrict equations ?x[t1..tn]=?x[u1..un]
up to conversion instead of up to unification. This (potententially)
looses constraints but this avoids looping at the time of considering
remaining problems and applying heuristics to them.
Also added printing of evar candidates in debugging evar printers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15061 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
change of semantics).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15060 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(see discussion on coq-club 5-6 Feb 2012).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15059 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- (Regular) Casts become typing constraints again.
- Coerce tycon to inductive type when applying bidirectional typechecking hint.
- Coerce lambda expressions to tycon, might require coercions now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15058 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- reinstall (x : T | P) binder syntax extension.
- fix a wrong Evd.define in coercion code.
- Simplify interface of eterm_obligations to take a single evar_map.
- Fix a slightly subtle bug related to resolvability of evars: some
were marked unresolvable and never set back to resolvable across calls
to typeclass resolution.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15057 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15055 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15053 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
There is no mention in the refman of relative search of the lib from the binaries directory and of the use of _CoqProject by CoqIdE.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15052 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
simpl was accessing the reduction stack at position n when
the length of the stack was exactly n.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15049 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It is now possible to tell simpl to unfold a constant
that hides no "match" but is applied to concrete arguments.
Arguments id _ !n.
Goal forall x, id x = id 2.
intros; simpl.
x : nat
========
id x = 2
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15048 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
TACTIC EXTEND block possibly parse the stand-alone name of a tactic,
then only the first rule must be registered in the atomic tactic table
so as to be consistent with what happens when the tactic is invoked
directly via its parsing rules and not via the interpretation of a
reference in the atomic tactic table. Concretely, this affects TACTIC
EXTEND blocks of the form
TACTIC EXTEND foo
[ "bar" tactic_opt(tac) -> ... ]
| [ "bar" constr_list(tac) -> ... ]
where both rules parses "bar" alone but only the first rule must be
registered in the atomic table,
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15046 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
printing occurrences list.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15044 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
"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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15039 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
of evars.
Used when interpreting a constr in Ltac: resolution is now launched if the constr
is casted.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15038 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15037 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
add_definition/fixpoint and parsing of the "Program" prefix.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
toplevel/
The code is not called yet from there.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15035 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15034 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Remove useless functorization of Pretyping
- Move Program coercion/cases code inside pretyping/, enabled according
to a flag.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
solutions to unification.
Only allow bidirectional checking of constructor applications, enabled by a program_mode flag:
it is backwards-incompatible due to delta-reduction, constructor parameters might get instantiated
with delta-equivalent but not syntactically equivalent terms.
Prepare for merging the Program-specific version of Pretyping/Cases/Coercion with the main code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15032 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15031 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15026 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Detyping is wrong about it and as far as I understand no one but Constrextern uses
it. Constrextern has now the same machinery for all patterns.
Revert if I miss something.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15022 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
|
|
univ_depends checks whether a universe variable appears or
is equal to a universe. In comparison with the previous hack
in inductiveops based on try...catching UniverseInconsistency,
this should be semantically equivalent, simplier, and more
robust in case we allow someday an unsafe mode where
merge_constraints would be a no-op.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15013 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Let's gain a few % by not using Pervasive.compare on a structure containing
some universe_levels, but rather UniverseLevel.compare on them.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15012 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unfocused proof (part of bug #2671).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15011 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
changes of the handling of unfocusing errors.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15010 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
+ Allowing much more function to be defined.
+ Using completely new algorithm to define non structural fixpoints
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15009 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15008 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Let's reintroduce the idea of stopping the graph traversal as
soon as a LE arc has been found, but this time we do so only
when we're not interested by the LT/LE distinction.
This way, we should remain correct but avoid largly the time penalty
induced by the last fix on univ.ml: the +30% on contrib Container
is almost gone, let's hope it'll be the same with Ssreflect.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15007 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15005 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15004 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
I love being push under presure to commit and do not try my fixup !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15003 85f007b7-540e-0410-9357-904b9bb8a0f7
|
