| Age | Commit message (Collapse) | Author |
|---|
|
The environment variable COQTOP has a different meaning for Coq
executables and for Coq Makefiles, which is troublesome when make
forwards it to subprocesses via the environment.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11366 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Correction divers messages d'erreur
- lorsque rien à réécrire dans une hyp,
- lorsqu'une variable ltac n'est pas liée,
- correction anomalie en présence de ?id dans le "as" de induction,
- correction mauvais env dans message d'erreur de unify_0.
- Diverses extensions et améliorations
- "specialize" :
- extension au cas (fun x1 ... xn => H u1 ... un),
- renommage au même endroit.
- "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize".
- "induction"
- intro des IH toujours au sommet même si induction sur var quantifiée,
- ajout d'un hack pour la reconnaissance de schémas inductifs comme
N_ind_double mais il reste du boulot pour reconnaître (et/ou
réordonner) les composantes d'un schéma dont les hypothèses ne sont pas
dans l'ordre standard,
- vérification de longueur et éventuelle complétion des
intropatterns dans le cas de sous-patterns destructifs dans induction
(par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas
le n dans le contexte),
- localisation des erreurs d'intropattern,
- ajout d'un pattern optionnel après "as" pour forcer une égalité et la
nommer (*).
- "apply" accepte plusieurs arguments séparés par des virgules (*).
- Plus de robustesse pour clear en présence d'evars.
- Amélioration affichage TacFun dans Print Ltac.
- Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu
(incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !).
- Fusion VTactic/VFun dans l'espoir.
- Mise en place d'un système de trace de la pile des appels Ltac (tout en
préservant certains aspects de la récursivité terminale - cf bug #468).
- Tactiques primitives
- ajout de "move before" dans les tactiques primitives et ajout des
syntaxes move before et move dependent au niveau utilisateur (*),
- internal_cut peuvent faire du remplacement de nom d'hypothèse existant,
- suppression de Intro_replacing et du code sous-traitant
- Nettoyage
- Suppression cible et fichiers minicoq non portés depuis longtemps.
(*) Extensions de syntaxe qu'il pourrait être opportun de discuter
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11102 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- MAJ CHANGES et COMPATIBILITY
- Réservation de || et && dans Notations.v
- code mort et MAJ suite commit 11072 (tactics.ml et changes.txt)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11073 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Ajout clause "in" à "remember" (et passage du code en ML).
- Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute
aussi une égalité pour se souvenir du terme sur lequel l'induction
ou l'analyse de cas s'applique.
- Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de
Programs qui avait la sémantique de "pose proof" tandis que le nouveau
a la même sémantique que "pose (id:=t)").
- Un peu de réorganisation, uniformisation de noms dans Arith, et
ajout EqNat dans Arith.
- Documentation tactiques et notations de tactiques.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11054 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Divers code mort (evarutil.ml, Bvector.v)
- MAJ perf-analysis
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11004 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
du filtrage. Cela permet de détecter les cas impossibles et de simuler
les contraintes d'inversion exprimables sous la forme d'un assignement
des arguments du constructeurs (cf le cas de Vtail dans Bvector.v).
Si l'on filtre sur t:I u1 .. un, et que chaque ui a la forme vi(wi)
avec vi composé uniquement de constructeurs, et que le résultat final
est P(w1,...,wn) (qui est éventuellement lui-même une evar) alors on
construit le prédicat
Q:=fun x1 .. xn y =>
match x1 .. xn y with
| v1(z) .. vn(z) t => P(z)
| _ .. _ _ => ?evar-speciale-cas-impossible
end
qui vérifiera bien que Q u1 .. un = P(w1,..,wp).
En raison de limitations de l'unification (on aurait besoin d'eta
conversion pour résoudre des problèmes du genre
"terme rigide == match x with _ => ?evar end", et besoin d'instanciation par
constructeurs pour des cas comme "A(y) = match ?evar with C x => A(x) end"),
je n'ai pas réussi à traiter le cas général.
Aussi, on adopte une stratégie pragmatique consistant à tester
plusieurs prédicats possibles :
- si un type final est donné, on essaie d'abord l'algorithme de
Matthieu et sinon le nouvel algorithme (permet par exemple de traiter
certains cas d'élimination dépendante de Bvector.v),
- s'il n'y a pas de type final, on essaie d'abord le nouvel algo et
sinon, on essaie avec un prédicat sans dépendance (permet de traiter
des cas compliqués comme celui de par cas sur I' dans le fichier
Case13.v de la test-suite).
Dans la pratique, il y a beaucoup de changement dans le code de compile_case.
- Par exemple, la compilation est maintenant toujours appelé avec un
prédicat (là où l'on pouvait avoir None, on a maintenant toujours au
moins une evar).
- En revanche, le membre droit des clauses est maintenant
optionnel. Si c'est None, c'est qu'on se trouve dans le cas d'une
branche impossible au moment du calcul du prédicat de retour.
- Aussi, on renonce aux PrLetIn et PrProd dans l'expression du
predicat de retour mais il faut savoir que c'est maintenant la liste
des tomatchs qui spécifie le contexte exact dans lequel le prédicat
de retour est bien typé.
- Et d'autres...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10883 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10880 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(i.e. "Inductive unit := tt." conduisait à "t:Prop" alors que le
principe de la hiérarchie d'univers est d'être cumulative -- et que
Set en soit le niveau 0).
Une solution aurait été de poser Prop <= Set mais on adopte une autre
solution. Pour éviter le côté contre-intuitif d'avoir unit dans Type
et Prop <= Set, on garde la représentation de Prop au sein de la
hiérarchie prédicative sous la forme "Type (max ([],[])" (le niveau
sans aucune contrainte inférieure, appelons Type -1) et on adapte les
fonctions de sous-typage et de typage pour qu'elle prenne en compte la
règle Type -1 <= Prop (cf reduction.ml, reductionops.ml, et effets
incidents dans Termops.refresh_universes et Univ.super).
Petite uniformisation des noms d'univers et de sortes au passage
(univ.ml, univ.mli, term.ml, term.mli et les autres fichiers).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10859 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- correction commit incorrect d'une modif de test-suite/success/apply.v
- réorganisation dev/
- renommage Print Modules en Print Libraries
- $Id:$ dans g_vernac.ml4
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10744 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10561 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10560 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10268 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10218 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
recommended way more explicitly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10050 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10012 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10010 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Documented in dev/doc/build-system.txt .
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9814 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in",
"erewrite" et "erewrite in". Correction au passage des bugs #1461 et
#1522).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(les let-in étaient comptés comme des produits, introduisant une incohérence
sur le nombre de produits à instancier dans les lemmes appelés par apply).
- Export simplest_eapply pour utilisation dans Sophia/RecursiveDefinition.
- Doc développeur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9785 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9390 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9322 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8946 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8857 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8856 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
'properties' de Subversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
en conséquence du Makefile dans dev/doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8750 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8140 85f007b7-540e-0410-9357-904b9bb8a0f7
|
