| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
ability to format inference rules (delimited by [[[ ]]]) and adds some
new flags. Here's the message from Chris:
- coqdoc now has support for inference rules inside coqdoc comments.
These should be enclosed in triple square brackets with the
following format.
[[[
|- t1 : Bool
|- t2 : T |- t3 : T
---------------------------- (T_If)
|- if t1 then t2 else t3 : T
]]]
The rule's name is optional. Multiple inference rules may be
included in the same [[[ ]]] block, separated by blank lines.
See http://www.cis.upenn.edu/~bcpierce/sf/Stlc.html#lab469
for some examples of the output. The output will only be pretty
in html - in other formats it is printed verbatim (though it
shouldn't be hard to add latex support, and I may soon).
- Two new coqdoc flags have been added. First, --inline-notmono
causes inline code to be printed in a proportional width font
(adjustable in the css file). Second, --no-glob tells coqdoc not to
look for .glob files (no links will be inserted for identifiers when
this flag is used).
- Finally, the handling of paragraphs and whitespace around lists
has been made somewhat saner.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13473 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13472 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13471 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13469 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13467 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
abstractions (reported by Pierre Courtieu).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13466 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
instances of the same variable name occur.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13465 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
flexible types what seems a reasonable strategy).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13464 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
- The code detected unused in notation.ml revealed a bug.
- In term.ml, restored a (short) useless function for
consistency/symmetry of the interface.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13463 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13462 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13461 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
|
|
|
|
|
|
| |
code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13459 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Set/Unset/Test. It allowed to document the behaviour of Local and Global on Set and Unset.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13456 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13455 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
This commit fixes a bug that made the system inconsistent with proof
irrelevance (the main idea being that Set = Prop by reflexivity).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13450 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
scheme was called on an unknown function anme).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13445 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
|
|
|
|
|
|
| |
of an anomaly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13442 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
'_a types
If there's no lambdas at the top of a constant body
and its type is functional
and this type contains type variable
and we're extracting to Ocaml
then we perform one eta-expansion to please the ML type-checker
This might slow down things, if some computations are shared
thanks to the partial application. But it seems quite unlikely to
encounter both situations (clever partial application and
non-generalizable variable) at the same time. Compcert is ok,
for instance.
As a consequence, no need for manual eta-expansion in AVL code
(and by the way MSetAVL.element wasn't a problem, it is monomorphic)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13441 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
this lacks robustness since "coqdoc -g" will drop away any commands unknown
from coqdoc, leading to possible synchronisation problems.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13440 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
revert the catch of anomalies in reductionops.ml now (commit 13353)?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13439 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13438 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13437 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
coqide doc link is the canonical link to last released version of
reference manual instead of link to corresponding coqide version).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13436 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
The patch does not address the possible use of evars by get_symmetric_proof in
unify_eqn. Someting has still to be done there.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13435 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
(see otherwise r12383). Seized the opportunity to remove useless
(v7-style syntax) parentheses in Match printing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13433 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
coqdep since it is now deterministic (later -R's overwriting former ones).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13432 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
too late, in a global environment which was no longer the correct one,
leading to the failure of error printing (hence an anomaly) in case
the command modified the state in several steps.
Now, errors raised by vernac commands are processed in the same
(intermediate) state they were raised from, just before rolling back
to the original state.
that modify the state in several
Now, errors raised by vernac commands that modify the state in several
steps (say S1, S2, ..., Sn) are processed in the state they were
produced in (S1, S2, ... Sn-1),
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13431 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13430 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
both for interpreting ltac patterns and patterns of "change pat with
term". In particular, in the current status, Goal evars needs
mandatorily to have the hole_kind GoalEvar. If this is too complicated
to enforce, we might eventually consider another approach to the
question of interpreting patterns in general.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13428 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
user either gives all missing arguments not dependent in the concl or
all missing arguments not *recursively* dependent in the concl (as
introduced by commit 13367). In practice, this means that "apply
f_equal with A" remains allowed even though the new, recursive,
analysis detects that all arguments of f_equal are inferable,
including the first type argument (which is inferable from the
knowledge of the function).
Sized the opportunity to better explain the behavior of clenv_dependent.
Also made minor code simplification.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13426 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13425 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Cf. coqdev for the details of the bug report.
- Protect some Hashtbl.find and other risky functions in order to avoid
as much as possible to end with an irritating Anomaly : Not_found.
- Re-enable in pp_ocaml_extern the case of a module-file used as
a module (e.g. module A' := A for A.v) when doing modular extraction.
- Rework the code that decides to "open" or not modules initially:
opening A when A contains a submodule B hides the file B even when
B isn't opened itself, we avoid that now.
- Fix some tables (sets or maps) used by extraction for which it is
critical to consider constants/inductives/global_reference _not_
modulo the equivalence of Elie, but rather via Pervasives.compare.
Still to do : avoid appearance of '_a in extracted code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13424 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- modules names can include quote '
- errors when parsing .mllib files are now properly reported
instead of dying ugly on some sort of Failure
- same when coqdep has to parse the output of ocamldep -modules
- lib/lib.mllib contains a typo (lowercase ident)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13423 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13422 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
+commit r13412
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13418 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13417 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
Introduces some hacks to have a consistent user experience. When coqtop
prints info on self then exit, return code is 2 if called with
-filteropts, 0 else
For now, no options are accepted by coqide. there is no way for now to
specify a filename that begins with a dash.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13415 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
See http://caml.inria.fr/mantis/view.php?id=4940
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13413 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13410 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13404 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
is now allowed on the left side of a match.
You can write 'match v with |Vnil => 0 |h :: q => 1 end.' if
'h :: q' stands for the vector 'Vcons _ h _ t'.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13403 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- generic iterator [iter] factorized in the same way as [same_level]
- as a consequence, remaining operations [mul] [compare] [div_gt]
are now defined and proved in a short and nice way and moved to
NMake.v.
- lots of other simplifications / factorisations in NMake_gen.
This file is still macro-generated, but is much shorter,
and the major part of it is now invariant.
- As advised by B. Gregoire, try to (re)create clever partial
applications in code of operators, in order to avoid projecting
ZnZ fields all the time in base cases. Case 0 can still be improved,
but it's already better this way :-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13402 85f007b7-540e-0410-9357-904b9bb8a0f7
|