| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8917 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
permettre de passer les occurrences en paramètre dans ltac, par exemple à pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8878 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive).
The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed.
The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have
a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready
for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml.
Subtac is now working as well as I demonstrated at TYPES.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8875 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
sig, sig2, sumor, list et vector dans Type
- Branchement de prodT/listT vers les nouveaux prod/list
- Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2
- Changements en conséquence dans les théories (notamment Field_Tactic),
ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8861 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8855 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8854 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
conséquences sur les .v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8852 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8831 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
Correction d'un bug dans add_glob (list_chop), avec ajout des list_drop_prefix dans lib/util.ml et de drop_dirpath_prefix dans library/libnames.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8768 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
clause in du cases
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8757 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
des inductifs de la clause "in" du filtrage.
- Débogage et extension du parseur xml (g_xml.ml4)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8755 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
l'option glob-dump
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8746 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
- Factorisation du procédé de transformation Cases -> RCases dans Detyping
- Rebranchement de la traduction XML pour Cases (interrompue depuis
suppression traducteur)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8741 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
PCase dans le type pattern: le type pattern est utilisé
essentiellement dans ltac, il est normalement obtenu sans typage, et
ce via rawconstr (sauf cas de filtrage ltac non linéaire où il est
obtenu de constr). Le cas d'un filtrage sur un "if" doit être traité à
part car sans le type, il est impossible de savoir le nombre
d'arguments du constructeur puisque par définition du "if", ceux-ci ne
sont pas liants et ne laissent pas dans la syntaxe concrète
(résolution au passage du bug #1070, dû à un filtrage incomplet dans
le passage de pattern à rawconstr permettant l'affichage des pattern).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8728 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
ce patch dispense d'ecrire le { struct .. }
En pratique, dans Topconstr.fixpoint_expr et Rawterm.fix_kind,
l'index de l'argument inductif devient un int option au lieu d'un int.
Les deux cas possibles:
- Some n : les situations autorisées auparavant, a savoir {struct}
explicite, ou bien un seul argument au total
- None : le cas nouveau, qui redonne un entier lors du passage de
rawconstr à constr si l'on trouve effectivement un unique argument
ayant un type inductif, et une erreur sinon.
Pour l'instant, on cherche l'inductif dans le type de manière
syntaxique, mais il est jouable de rajouter un poil de reduction
(au moins delta).
Dans le détail, voici les coins que ce patch influence:
- parsing/g_xml.ml4: continue pour l'instant a attendre un index
explicite via un element xml "recIndex"
- contrib/interface/xlate.ml: a priori ca marche, car il y avait déjà
un cas ctv_ID_OPT_NONE correspondant à l'absence de struct. Par
contre, dans le détail, le code pour un CFix utilise l'index de
recurrence pour recouper au besoin le type du fixpoint en deux.
Est-ce que je me gourre en supposant que si l'on a besoin de couper
ainsi ce type, c'est qu'il provient non pas du parseur Coq, mais de
l'impression d'un constr, et donc que l'index aura été correctement
résolu ?
- contrib/subtac/subtac_command.ml:
- contrib/funind/indfun.ml:
dans les deux cas, j'ai fait le service minimum, le struct reste
obligatoire s'il y a plusieurs arguments. Mais ca ne serait pas
dur à adapter pour ceux qui comprennent ces parties.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists.
Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop.
- Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8675 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
uses the original Coercion implementation.
Updated contributions that called pretyping to use the default impl.
Also update subtac using the functor, do some renamings and add interfaces for all files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
7833, et que la révision 8644 n'avait pas corrigé dans le bon sens;
renommage en mind_consnrealdecls pour éviter la confusion de sens
avec mind_nrealargs
- Correction de la description du type one_inductive_body
- Ajout test avec let-in dans params et dans type constructeur
(fichier Case12.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8653 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
May cause make world to fail because of dependency problems, make depend clean
world should fix that (hopefully).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8125 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7985 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
dans la mesure où le nom d'un module est différent selon qu'on est en
cours de compilation (MPself) ou requis (MPfile)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7984 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7967 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
l'inductif si clause "in I ...") dans Constrintern, pour assurer
notamment que les constructeurs et inductifs dans pattern (obtenu de
rawconstr) ont les bonnes arités
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7954 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7946 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
eq_rawconstr in topconstr to prepare the introduction of the new
version of functionnal induction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7928 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
changé entre les version 3.08.4 et 3.09.0 (influe notamment sur l'ordre
d'application des Hints de auto)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7925 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7881 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7879 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7842 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7838 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
et d'"externalisation"; standardisation du nom des fonctions d'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
déplacement dans Topconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7826 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7823 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
traitement dans alias de motifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7821 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
peuvent maintenant être définies au niveau utilisateur) + divers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7820 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
filtrage + prise en compte de notations numérales définies au niveau utilisateur+ légère restructuration
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7819 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7817 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
suppression des coercions permet aussi d'afficher un nombre, on choisit l'affichage qui n'introduit pas de délimiteurs si possible (exemple: avec 'Zpos 2', si Zpos est une coercion, on peut effacer la coercion et afficher 2 dans le type positive, ou bien garder la coercion afficher 'Zpos 2' comme 2 dans Z; dans certains cas - cf 4CT - il n'y a pas d'afficheur qui gère la coercion et il faut la retirer avant d'appliquer l'afficheur de nombre le plus interne)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7796 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
aussi avant l'affichage des notations primitives
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7788 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
l'activation à l'import des notations qui ne sont pas des définitions syntaxiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7779 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
de chaîne de caractères tel que "foo"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7762 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7758 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7739 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
|
herbelin
msozeau
notin
letouzey
bertot