| 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@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
inductiveops vers pretyping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6029 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5710 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
le if-then-else
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5706 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5596 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
sont supposes sans dependances en les arguments des constructeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5589 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
fixes s'affichent correctement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
reste a transporter les loc dans check_fix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5292 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
des dependances de nom
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5283 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
que les variables liees sont toujours nommees
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5268 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
pour eviter la confusion avec la (vraie) application
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5114 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4948 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4789 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4499 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
indépendant des globaux quand hors but (on garde l'évitement des globaux en but, pour compatibilité)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4458 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4345 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4338 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4336 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4264 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Option -v8 à coqtop lance coqtopnew
Le terminateur reste "." en v8
Ajout construction primitive CLetTuple/RLetTuple
Introduction typage dans le traducteur pour traduire les Case/Cases/Match
Ajout mutables dans RCases or ROrderedCase pour permettre la traduction
Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts
+ Bugs ou améliorations diverses
Raffinement affichage projections de Record/Structure.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
les metavariables de patterns; fusion NoHypId et Hyp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4043 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
Utilisation d'ident plutôt que int pour PMeta/CPatVar
Ajout CEvar pour la saisie des Evar
Pas d'entrée utilisateur pour les Meta noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4009 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
constrextern.ml est l'équivalent de termast.ml pour le nouveau
printer; topconstr.ml; contient la définition de "constr_expr";
modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2987 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2829 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2827 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2809 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2808 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
définies
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2633 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2630 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
par l'absurde
- un open_constr est maintenant un terme accompagne du sigma dans lequel il
est typable (il manquait l'info concernant le contexte de typage des
nouvelles evars)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2579 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
definies y apparaissait
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2486 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
- coqtop -byte -opt bouclait!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2435 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
mal nommé dans findtype
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2303 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
(suite)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2295 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2293 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
du Cast
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2214 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2199 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2198 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2176 85f007b7-540e-0410-9357-904b9bb8a0f7
|