| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13511 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Pratical situation: simple eapply foo on a goal ?123, while foo is a
(forall f, exists ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13479 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
Instead of the full Evd.fold, Evd.fold_undefined seems enough in
- Evarutil.push_dependent_evars
- the nf_evars call in Evarutil.evars_to_metas
(we hence create a function nf_evars_undefined and use it there)
This should bring back Compcert into reasonable compilation time
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13478 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
the wish to allow named projections to not be put in the canonical
structures databases for Structures.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13474 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Functions from Termops were sometimes fully qualified, sometimes not
in the same module. This commit makes their usage more uniform.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13470 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
These functions are applied much more often without labels than with
them (the alternate of adding the label wherever relevant changes 124
lines instead of 41). Moreover, this is more consistent with the Term
module and there is no ambiguity in argument types. This commit goes
towards elimination of occurrences of OCaml warning 6.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13468 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
In particular, the unused lib/tlm.ml and lib/gset.ml are removed
In addition, to simplify code, Libobject.record_object returning only the
('a->obj) function, which is enough almost all the time.
Use Libobject.record_object_full if you really need also the (obj->'a).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
governed in the latter case by a flag since (useful e.g. for setoid
rewriting which otherwise loops as it is implemented).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13443 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- improving error message when a reference to unfold is not found
- repairing anomaly when an evaluable reference exists at
internalisation-time but not at run time, and similarly for an
arbitrary term (but the latter is new from 8.3 because of the new
use of retyping instead of understand for typing Ltac values)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13408 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
dependent arguments. It breaks compatibility as some [apply with]
clauses are not necessary anymore. Typically when applying [f_equal],
the domain type of the function can be infered even if it does not
appear directly in the conclusion of the goal. Fixes bug #2154.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13367 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
terms, but an anomaly instead. It is caught in pretyping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13353 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
predicate in branch read-back (2)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13350 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- Document and fix [autounfold]
- Fix warning about default Firstorder tactic object not being defined
- Fix treatment of implicits in Program Lemma.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13334 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- Moved Global Set from Keep to Substitute to ensure it is activated
in real time and not only after the main parts of the module
- Renamed Importation into Import in option name
- Made "Print Libraries" prints the modules in the importation order
(which is the most relevant order for non-commutative declarations)
instead of load order
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13318 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Added support for recursive notations with binders
- Added support for arbitrary large iterators in recursive notations
- More checks on the use of variables and improved error messages
- Do side-effects in metasyntax only when sure that everything is ok
- Documentation
Note: it seems there were a small bug in match_alist (instances obtained
from matching the first copy of iterator were not propagated).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13310 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13225 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
them. This was the cause of the failure of compilation of
CyclicAxioms after "replace" starting supporting open constrs (r13206).
Seized the opportunity to clean a little bit things around nf_evar,
whd_evar, check_evars, etc.
Removed obsolete printer mod_self_id from dev/db.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
r13080 via a failure in CoRN (pattern_of_constr needs correct sigma).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13205 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Printer pr_cs_pattern is kept in recordops only. Also updated CHANGES.
Fixed spelling of "uniform inheritance condition" in doc too (see
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13204 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
proof of Chung-Kil's Hur Heq package): conversion in "trivial_unify"
accepted evars as ordinary variables. I hope I did not invalidate some
features that would have needed restricting conversion on evar-free
terms, but since failure of conversion in presence of evars is redirected
to the main unification algorithm, I guess it is OK.
For better readibility, I also inlined and cleaned a bit trivial_unify.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13193 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13179 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Applied it to fix mli file headers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13167 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
by a regular error in v8.3.
Example behaves better in trunk thanks to new proof engine. In fact,
there are two distinct solutions to a unification problem: should
"refine" commit to one of them or leave the problem open? For trunk,
improved the unification error message by enforcing nf_evar (but at
some time, nf_evar in error messages should move to himsg because it
is costly when errors are used for backtracking).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13127 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- made the example work (a call to whd_meta was missing)
- replaced the internal error messages of w_unify_to_subterm_list into
user-understandable messages
- incidentally fixed the meaning of whd_meta (which now takes an evd)
and meta_name (which now does what it means and do not treat differently
the instantiated metas)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13122 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
More precisely, the mecanism used to automatically infer return
predicates of the form
"as x in I y1..yn match y1..yn x with u1(z1)..un(zn) => P(z1..zn) | _ => ID end"
now computes the dependencies in the types of y1..yn and x. This
allows it to benefit of the generalisation mechanism of the
pattern-matching compilation algorithm ("Abstract") and to infer more
sophisticated return predicates (e.g. when working with "vector").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13118 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
substitution of evars when solving equation "?n[subst] = t": this is a
quite common useful heuristic for inferring the return predicate of "match".
Made incidentally a minor simplification of expand_full_opt.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13117 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13116 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Use two ways to solve it:
- added a whd_betaiota in solve_simple_eqn (since evarconv itself
refuses beta to preserve the opportunities of first-order-matching
expressions of the form "(fun x => P) t"; an advantage of this
whd_betaiota is also that it may simplify K-redexes.
- also added a last-chance test in case of failing occur-check by
trying to fully head-normalize (with delta) the right-hand-side
(allows to solve for instance "?n = id ?n" where id is a constant
(a bridled form of solve_refl that use fconv instead of evar_conv_x).
Incidentally improved a bit the rendering of the type of generalized
terms in pattern-matching by using whd_betaiota.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13113 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- first bug was a missing lift when the return predicate was assumed to be
a simple evar
- second problem was in the inference of a custom inversion predicate in
case of matching on a term in a constrained type (like "vect (S n)"):
the rel bound to local definitions in the instance of evars where
instantiated (by other evars) which is wrong per se but which contradicted
the assumptions of find_projectable_vars in evarutil.ml which assumed that
this did not occur; solved the problem by not instantiating references to
local definition which (probably) will not loose some opportunity of
unification in presence of non unfolded local definitions, ...
- also cleaned a bit prepare_predicate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13112 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Instances found by matching.ml now collect the set of bound
variables they possibly depend on in the pattern (see type
Pattern.extended_patvar_map); the variables names are canonically
ordered so that non-linear matching takes actual names into account.
- Removed typing of matching constr instances in advance (in
tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback
is that we may have to re-type several times the same term but it is
necessary for considering terms with locally bound variables of which
we do not keep the type (and if even we had kept the type, we would have
to adjust the indices to the actual context the term occurs).
- A bit of documentation of pattern.mli, matching.mli and pretyping.mli.
- Incidentally add env while printing idtac messages. It seems more correct
and I hope I did not break some intended existing behavior.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13080 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13028 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Evars of source "ImpossibleCase" that remain undefined at the end of
case analysis are now defined to ID (forall A : Type, A -> A).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13023 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The choice between camlp4/5 is done during configure with flags
-usecamlp5 (default for the moment) vs. -usecamlp4.
Currently, to have a full camlp4 compatibility, you need to change
all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
into "`EOI" in grammar entries. I've a sed script that does that
(actually the converse), but I prefer to re-think it and check a few
things before branching this sed into the build mechanism.
lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
and try to propose a common interface (cf LexerSig / GrammarSig).
A few incompatible quotations have been turned into underlying code
manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
parsable by both camlp4 and 5. See in particular the fate of
<:str_item< declare ... end >>
Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
This forces to use camlp5 > 5.01.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
These declarations (e.g. make -C .. bin/coqtop.byte) are quite
annoying when debugging stuff over the whole archive: all of a
sudden, M-x recompile isn't doing what you intended just because
you've visited some specific files. Instead:
- Feel free to rather add intermediate targets in the Makefile if
they aren't there yet.
- For avoiding typing the -C with many .. after, you can have a
look at my recursively-descending make:
http://www.pps.jussieu.fr/~letouzey/download/make.sh
which is to be renamed make and placed in a bin dir with more
priority than /usr/bin. Beware! I've already add a few bad surprises
with this hack, but it's really convenient nonetheless.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13014 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13013 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
In "(match ... with |... -> fun x -> t end) u", "x" has now the subterm
property of "u" in the analysis of "t".
Commutative cuts aren't compatible with typing so we need to ensure that
term of "x"'s type and term of "u"'s have the same subterm_spec.
Consequently,declaration.MRec argument has changed to the inductive name
instead of only the number of the inductive in the mutual_inductive
family.
In subterm_specif and check_rec_call, arguments are stored in a stack.
At each lambda, one element is popped to add in renv a smarter
subterm_spec for the variable. subterm_spec of constructor's argument
was added this way, the job is now done more often.
Some eta contracted match branches are now accepted but enforcing
eta-expansion of branches might be anyway a recommended invariant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13012 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
evar_map into a map for defined evars and a map for undefined evars.
Even before Spiwack's new proof engine, some Evd.fold were very
costly, e.g. in check_evars or progress_evar_map. With the new proof
engine, undefined evars traversals are apparently even more common (at
least, it improves significantly the complexity of some calls to omega
in JordanCurveTheorem - a new factor 5-7 after the factor 5-6 obtained
by removal of evar_merge in clenv_fchain in commit 13007, arriving to
figures comparable to the 8.3 ones).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13011 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13005 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- coq logo isn't destructed anymore
- Erase debug printers not implemented for new proofs
- ocamldoc compatible comments for pretyping/rawterm.mli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12988 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
dev/ocamlweb-doc has been erased. I hope no one still use the
"new-parse" it generate.
In dev/,
make html will generate in dev/html/ "clickable version of mlis". (as
the caml standard library)
make coq.pdf will generate nearly the same awfull stuff that coq.ps was.
make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of
the given directory.
ocamldoc comment syntax is here :
http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html
The possibility to put graphs in pdf/html seems to be lost.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
- git ignore g_decl_mode.ml
- exhaustive match for pp_vernac (BeginSubproof, ...)
- for ocamlbuild, remove a spurious cycle in recordops.mli
(unnecessary open of Classops), and fixes of *.itargets and _tags
The compilation via ocamlbuild still need some work, since
plugin firstorder now depends on the new plugin decl_mode
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12964 85f007b7-540e-0410-9357-904b9bb8a0f7
|