| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9831 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
details).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
discussion avec Georges)
- La notion d'insertion maximale n'est plus globale mais attachée à
chaque implicite
- Correction de petits bugs dans le calcul des implicites
- Raffinement de la notion "sous contexte" pour l'affichage des coercions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9817 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- correction du mode strict qui n'était pas si strict,
- option "Set Strong Strict Implicit" pour activer le mode strictement
strict (désactivé par défaut pour raison de compatibilité),
- option "Set Reversible Pattern Implicit" pour activer les implicites
inférables par unification-pattern (désactivé par défaut par compatibilité),
- option "Unset Printing Implicit Defensive" pour désactiver
l'affichage des implicites n'ayant pas été décelés stricts,
- option "Set Maximal Implicit Insertion" pour que les
applications soient saturées en implicites si possible,
- une optimisation du mode non strict pour que l'algo de
recherche des implicites renonce à calculer les occurrences non
strictes qui pourraient avoir à être affichées dans le mode défensif,
avec pour conséquence que le mode défensif, pour celui qui le veut,
devient a priori encore plus verbeux, ex:
Set Implicit Arguments.
Definition id x : nat := x.
Parameter f : forall n, id n = id n -> Prop.
Check (f (refl_equal O)).
(* Affichait: "f (refl_equal 0)" mais affiche maintenant
"f (n:=0) (refl_equal 0)" *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9812 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9809 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
delta-reduction at fonctor application.
Example:
Module Type S.
Parameter Inline N : Set.
End S.
Module F (X:S).
Definition t := X.N.
End F.
Module M.
Definition N := nat.
End M.
Module G := F M.
Print G.t.
G.t = nat
: Set
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9782 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Set Elimination Schemes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9780 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
scope.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9734 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
obligations (even an opaque one).
Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes.
Various little subtac changes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9707 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
le parser
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9706 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9693 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
compile-verbose +
ajout Pp.strbrk pour faciliter les césures faciles + messages divers).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9678 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9677 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
+ petit nettoyage himsg.ml + petite uniformisation erreurs CannotUnify
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9668 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
implicites des Fixpoint/CoFixpoint (report revision 9617 de 8.1 vers trunk)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9618 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
rapport de bug #1225 -- qui reste ouvert sur le fond)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9527 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Makefile: Option (environment variable NO_RECOMPILE_LIB) to not
recompile the whole standard library just because the coq binaries
got rebuilt.
- Infrastructure to change the object pretty-printers at runtime.
- Use that infrastructure to make coqtop-protocol with Pcoq trees and
Pcoq-protocol with pretty-printed terms possible in coq-interface.
- Make "Back(track)" into closed sections, modules and module types
"Just Work™".
- Modernise/generalise Pcoq protocol a bit, make some of its warts
optional.
- Implement "Show." in Pcoq mode.
- Add Rpow_def.vo to REALSBASEVO so that its dependencies are
computed (and used).
- "make revision" now handles GNU Arch / tla in addition to svn.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Avant : une unique méthode discharge_function qui avait accès à l'ancien
environnement mais pas de possibilité de raisonner avec les objets
du nouvel environnement en cours de construction. C'était problématique
pour le discharge des implicites, arguments scope, etc qui étaient
finalement faits en même temps que le discharge des constantes et inductifs
mais avec pour effets de bord que les entrées dans la lib_stk arrivaient
juste avant celles des constantes et inductifs avec des problèmes pour
effacer les bonnes entrées au moment du reset
- Maintenant : deux méthodes distinctes : discharge_function qui est appliquée
pour collecter de l'ancien environnement ce qui est à garder dans la
section et rebuild_function qui reconstruit le nouvel environnement
connaissant déjà les nouvelles valeurs des objets précédants (on se rapproche
ainsi plus de la méthode en deux temps d'avant la 8.1 tout en offrant
l'extensibilité que la méthode ancienne du fichier discharge.ml ne
permettait pas)
Au passage, ajout d'un modificateur Global aux déclarations
d'implicites et d'arguments scopes pour indiquer qu'elles doivent
perdurer à la sortie de la section
Au passage, suppression de l'objet DISCHARGED-HYPS-MAP et intégration
aux objets VARIABLE/CONSTANT/INDUCTIVE (seule la table des hyps
discharged reste)
Au passage, nettoyage impargs.ml, suppression code mort résiduel du
traducteur etc...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9474 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
current state.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9464 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
conjunction of mutual inductions principles.
e.g: Combined Scheme mutind from tree_ind, forest_ind gives a conclusion (forall t : tree, P t) /\ (forall f : forest, P0 f).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9461 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
plus simples)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9446 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9416 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
sortie de session (nécessite option -batch)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9414 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9402 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
chemin physique : expansion uniquement pour Load, Add LoadPath, Declare ML
Module, Cd, ... mais pas pour les options -I, -boot, -R, -load-vernac-file, ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9398 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9384 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9333 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
(suppression au passage d'un cast dans constant_entry_of_com - ce
n'est pas normal qu'on force le type s'il n'est pas déjà présent mais
en même temps il semble que ce cast serve pour rafraîchir les univers
algébriques...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
"Dump Universes"), "Universe inconsistency", et description brève des univers
algébriques.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9306 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9304 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9261 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9259 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
ligne relatif à la ligne au lieu de absolu par rapport à la session)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9252 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9227 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
d'un constr c, on vérifie que c est clos dans l'environnement de m (#1183)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9217 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
xml-like patterns (<prompt></prompt>).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9191 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9176 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9147 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
en dernière étape de la procédure d'unification
- Nouvelle fonction consider_remaining_unif_problems dédiée à la résolution
de l'unification premier ordre flexible/rigide
- Déplacement check_evars dans Evarutil
Question ouverte: que faire pour l'unif premier ordre flexible/semiflexible ?
(cf exemples d'application dans test-suite/success/evars.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9141 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9133 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
(après tout, d'autres exemples de non totalement mutuels sont acceptés
sans problème par la test de bonne fondation - cf add1/add2 dans
Sophia-Antipolis/MATHS/GROUPS/Z et Sophia-Antipolis/HARDWARE)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9128 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
récursifs parce ce que la condition de garde élimine les appels
récursifs sur des sous-termes qui, par construction des types
inductifs, ne peuvent ultimement retomber sur un objet du type initial
de l'argument de décroissance (p.ex. un appel récursif sur p:positive
provenant d'un filtrage sur un z:Z ne sera d'emblée pas considérer
sous-terme car la destruction d'un positive ne donnera jamais un Z --
cf exemple de addZ dans une version d'avant aujourd'hui de
Sophia-Antipolis/MATHS/GROUPS/Z/Zadd.v).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9126 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
(+ uniformisation position notation dans les blocs inductifs et récursifs)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9110 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Relâchement de l'exigence que les types des paramètres et le type
des (co-)points fixes soient donnés. Ils peuvent maintenant être
inférés à partir des autres informations de types.
- Plus de déclaration séparée de celles des fonctions d'un bloc de
points fixes qui n'interviennent pas dans la définition des autres
(collect_non_rec): remplacement par un simple warning en cas de non
dépendance mutuelle de toutes les fonctions du bloc (de toutes
façons les fonctions qui intervenaient dans les autres sans en
dépendre - càd les fonctions définissables avant la partie point
fixe - n'étaient pas détectées)
- Ajout du test de dépendance mutuel au cas des co-points fixes
Extension et réorganisation de l'interprétation des blocs de
définitions (co-)inductives: relâchement de l'exigence que les types
des paramètres soient donnés. Ils peuvent maintenant être inférés à
partir des autres informations des blocs d'inductifs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9108 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9104 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9092 85f007b7-540e-0410-9357-904b9bb8a0f7
|