| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14557 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14556 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14555 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
When adding an inductive block in the environment, we now check that
no types or constructors in this block correspond to a label already
used in the current module. The earlier check was to try only the
first inductive type (which serves as label in the structure_body),
that was causing awkward situations, cf. for instance #2603.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14553 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14552 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14551 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14550 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
second-order matching) which was not working correctly in the general
case.
Also made that second-order matching for tactics (abstract_list_all)
uses this algorithm, along the lines of a proposal first experimented
by Dan Grayson (see unification.v).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14549 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
This is now fixed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14548 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
for the functions of unification.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14547 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14546 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
Most of the time, a constant name is built from:
- a kernel_name for its user part
- a delta_resolver applied to this kernel_name for its canonical part
With this patch we avoid building unnecessary constants for immediately
amending them (cf in particular the awkward code removed in safe_typing).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14545 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Inductive definitions aren't that big, but they may contain some
constr (in types, rel_context, etc), hence if we hash-cons the
constr in Definition but not these ones, we may loose some sharing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14544 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14543 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is just a minor detail, but if we take care to use in mkRel
always the same physical Rels for n <= 16, then let's ensure that
these Rels are preserved by hash-consing. This way, we avoid
killing some sharing during hash-consing of most of constr but not
all (for instance those in mind).
In fact, this is probably superfluous since earlier commit
about "| Rel n as t -> t", but let's be sure.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14542 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14541 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Since we hash-cons arrays in place, no need to re-allocate
a few structures around them.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14540 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Compute chain of aliases once for all so as to simplify code.
- In is_unification_pattern, expand all vars/rels of the unification
problem until they are no longer vars/rels so that the list of
vars/rels used in the rhs is correct, and, the list of arguments of
the evars eventually become irreducible vars/rels (in particular,
this solves bug #2615).
- Some points remain unclear, e.g. whether solve_evar_evar should
reason with all let-in expanded or with let-in expanded only up
to the last expansion which is still a var or rel.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14539 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
problems with dependencies. Generalized it to matching over dependent
tuples as explored by Dan Grayson. Currently used only in Evarconv.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14538 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
by the way renamed into materialize_evar.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14537 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
(replace_vars was anyway optimized)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14536 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14535 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
evar_define so that it can recursively deal with evar/evar problems.
Also, check_evar_instance now called after each instantiation.
Also did a bit of file reformatting.
The commit apparently induces a loss of some 0,4% on the compilation
of the standard library. Maybe, introducing a heuristic to decide when
to call check_evar_instance (which I guess is responsible for the
overhead) might be a good thing to look at?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14534 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14533 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Thanks to Tom Prince for spotting this
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14530 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
when schemes are generated for internal use of Coq.
Ideally, I would like to add these names asynchronously in name spaces
relevant for the corresponding inductive type, what modules do not
support since modules cannot be reopened.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14529 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
Maybe could we keep only the kernel check, but message would
certainly need to be reformulated then.
For instance, the message was previously different for an attempt to
redefine a name whether this name was in the same section or not.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14528 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Btw, we also get rid of equalities on something else than elements or sets
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14525 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14524 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14523 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
it properly in the syntax of terms
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14522 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- We now handle things like (H : E.eq x x -> ...) by rewriting
E.eq x x into True.
- There was also a confusion between E.t and its various equivalent
(but syntactically different) forms. This should be solved by
preventing inlining during an inner functor application.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14520 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
See bug #2614.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14519 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
The changes to myocamlbuild.ml didn't compile.
See bug #2614.
Signed-off-by: Tom Prince <tom.prince@ualberta.net>
Signed-off-by: Stephane Glondu <steph@glondu.net>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14518 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
There were some confusion on the role of clear_proofs which was
applicable only to the global named_context. Hopefully made things
clearer.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14517 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
instance of the initial pattern (this fixes compilation of CoRN after
r14499).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14516 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
If two distinct parameters of the inductive type contributes to
polymorphism, they must have distinct names, othewise an aliasing
problem of the form "fun x x => max(x,x)" happens.
Also insisted that a parameter contributes to universe polymorphism
only if the corresponding occurrence of Type is not hidden behind a
definition.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14511 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
to ensure not only that several passes are done and the references are
correct but also to avoid one of the targets Reference-Manual.dvi or
Reference-Manual.pdf reading .aux files modified concurrently by the
other target.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14510 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
constraints
Patch by Robbert Krebbers (cf. #2611)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14509 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
that the return predicate of the match construction is at an allowed
sort, resulting in tactics possibly manipulating ill-typed terms. This
is now fixed,
Incidentally removed in pretyping an ill-placed coercion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14508 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- An inductive is hidden inside case_info.
(btw, maybe we could get rid of this ci_ind altogether,
since the information is already in the predicate of the match)
- Typical situation where user kn and canonical kn are initially (==)
was not preserved by hconsing of constant / mutual_inductive
- inductive = (mutual_inductive * int) and
constructor = inductive * int were not properly shared
This should fix the strange situation of Udine/PiCalc taking *more*
vo space after the last round of hcons tweaks.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14507 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14506 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
obfuscate the standard library.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14505 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
polymorphic and only for inductive polymorphic types is the conclusion
of the arity irrelevant. Refreshing at discharge time (that
indtypes.ml expects for retyping) should be done only for polymorphic
types. For monomorphic inductive types in Type, the type level is
possibly related to universe constraints stored in the section and it
must not be changed. [Alternatively, discharge should not retype
inductive types from scratch, but instead generalize them over the
section variables, the same way it does for definitions/axioms. But
that's another story.]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14501 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
I assume that once Coq is installed in non-local mode and run from its
installed path, sources are no longer available. The coqsrc variable
doesn't make any sense, then, and its intended value can always be
inferred from Sys.executable_name. Moving it to Envars.coqroot.
Make coqlib optional. Currently, it is set to None only in -local mode
or with ocamlbuild. When set to None, -local layout is assumed
(binaries in ./bin, library in .). The behaviour should not be changed
when an explicit coqlib has been given to ./configure.
This commit should make it possible to run a Coq compiled with -local
from anywhere (no hard-coded absolute path embedded in the
executables, intermediary step to bug #2565). It WILL BREAK settings
re-using source trees after installation in non-local mode (are there
actual use cases for that?).
Hard-coded absolute paths still remain:
- in the build system, so the need to re-run ./configure after moving
the source tree is still expected for now;
- in coqrunbyteflags, I think we are limited by ocaml itself;
- docdir.
All absolute paths should be removed, ultimately.
As a side-effect, simplify computing of Envars.coqbin. I don't see any
good reason to keep it as a function.
Disclaimers:
- initialization of Sys.executable_name is not consistent across all
architectures; relying so much on it might trigger bugs. I'm pretty
sure something will explode if one adds arbitrary symlinks on top of
that;
- ocamlbuild stuff not tested.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Tactics set/remember and destruct/induction take benefit of it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14499 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
function but also restricting it to closed matching and consequently
renaming it to subst_closed_term_occ.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14498 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14497 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
resolution from Tacinterp to Pretyping (close to resolve_evars) so
that final evar resolution can eventually be called from Tactics.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14496 85f007b7-540e-0410-9357-904b9bb8a0f7
|