| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6064 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6050 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
either c1 with c2 or c2 with c1 (if c1 did not occur in the goal).
The new implementation will not do it. Thus I am replacing every occurrence
of (setoid_replace c1 with c2) with
(setoid_replace c1 with c2 || setoid_replace c2 with c1).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6047 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
always None) removed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5967 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5965 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
fatale d'ocaml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5958 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5951 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5904 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
(the HELM/MoWGLI stylesheets do not longer require it)
* helm:helm_link added to each <a/> element whose href is an URI
* the required <body/> element was not generated for theories
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5877 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
type inference for inferred types) undone. Previous performance restored.
- bug in cic2acic (code that used to be dead fixed): the type of a sort
was computed as the sort itself
- CPropRetyping in cic2acic modified to handle correctly the sort Set in
the two cases Predicative Set / Impredicative Set
- CPropRetyping.get_type_of used in place of Retyping.get_type_of everywhere
in cic2acic. This closes (again, but more efficiently) the bug about
CProps erroneously recognized as Types in inferred types
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5875 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Motivation: the inner sorts computed for the inner types were computed
by Coq itself. Thus Nijmegen's CProp was exported as Type. To export CProp
as CProp I have to implement a CProp-aware single type inference.
To avoid the reimplementation I use double type inference.
* Known problems: the double type inference algorithm is slower than the
usual type inference algorithm. Moreover too many types and sorts are
computed in this way. As a consequence the exportation module is now
much slower (the exportation time seems to be doubled in the average
case).
In the future I will try to restore the original performances.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5872 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
exported as a copy of the variable id. Fixed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5865 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5857 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5849 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
mind_record
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5836 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
DTDs licence is still GPL. This should create no problem.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5828 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5825 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
sa signature
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
incompatible avec la sémantique précédente qui identifiait "Z_of_nat x * Z_of_nat y" avec "Z_of_nat (x * y)"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5774 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5744 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
de toutes façons inutile)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5733 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5695 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5661 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Coq (the latest verion can be retrieved from the HELM and MoWGLI pages).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5658 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
- copyright notice inserted in every DTD
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5657 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
generates not well-formed XML files). An hook is left in xmlcommand.ml
to register a pretty-printer function once a fixed implementation is provided.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5656 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
(they used to be exported as products of sort Type).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5652 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
^ ... ^ special verbatim code also backtracked.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5651 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
with non dependent products. The main motivation is that inductive definition
parameters often occurs as non-dependent products in the product types,
but the binder names are still necessary to render the definition in the
usual Coq way.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5646 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
HTML tags (i.e. # ... #), strong verbatim tags must be now used (i.e. ^ ... ^).
WARNING: it requires the fortcoming commit on coqdoc to work properly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5644 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
in .v files. The exportation module produces generic XML ==> the character
entities that were verbatim copied were never declared and the generated
files were not well-formed XML files. Fixed by adding to the internal subset
of the DTD an inclusion to the three files were the (X)HTML entities are
defined. Due to technical reasons (HELM Getter URL rewriting), the chosen
URL refers to the HELM web site.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5636 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5635 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
DTD Change.
ht:DEFINITION/Definition differentiated into
ht:DEFINITION/Definition and
ht:DEFINITION/InteractiveDefinition
because of an explicit request of Iris Loeb.
HELM/MoWGLI DTD and Stylesheet changed accordingly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5634 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
DTD. Used for local proofs (e.g. "Let x : True. auto. Qed.").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5630 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
and not as variables. Partially fixed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5629 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
This avoids stdout cluttering in interactive mode.
Whenever verbose is set to true, all the strings sent to
the Buffer are also printed on stdoud.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5628 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5627 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
un record; restructuration en consequence
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5623 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
The idea is:
1. constructors are always declare by hand by the user ==> binders always
have a meaning.
2. the binders are fundamental for record fields, even if the dependent
product is really non-dependent.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5621 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
@name of ht:SECTION renamed in @uri
Its semantics has not changed (it is the base URI of relative URIs defined
inside the section).
HELM/MoWGLI stylesheets updated accordingly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5619 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
*_subproof)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5617 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5614 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5613 85f007b7-540e-0410-9357-904b9bb8a0f7
|