aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Désactivation du test du printer arithmétique v7Gravatar herbelin2004-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6442 85f007b7-540e-0410-9357-904b9bb8a0f7
* travail sur les types extraitsGravatar letouzey2004-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6441 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2004-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout bug do_restrict_hypGravatar herbelin2004-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6438 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug historique de do_restrict_hyps + code mortGravatar herbelin2004-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6437 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug historique de do_restrict_hyps + code mortGravatar herbelin2004-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6435 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs dans la déclaration du type du terme filtré si non définiGravatar herbelin2004-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6433 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug nom exceptionGravatar herbelin2004-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6432 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2004-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6430 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2004-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6429 85f007b7-540e-0410-9357-904b9bb8a0f7
* * added subst_evaluable_referenceGravatar sacerdot2004-12-07
| | | | | | | | * the Unfold hints of auto/eauto now use evaluable_global_references in place of global_references git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6428 85f007b7-540e-0410-9357-904b9bb8a0f7
* The type Pattern.constr_label was isomorphic to Libnames.global_reference.Gravatar sacerdot2004-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6427 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation du nom d'entrée openconstr en le nom du type open_constrGravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Erreur commit précédentGravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6425 85f007b7-540e-0410-9357-904b9bb8a0f7
* Garder les cast semble décidément le meilleur moyen de rester synchrone ↵Gravatar herbelin2004-12-06
| | | | | | avec l'environnement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6424 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des cast après avoir utiliser l'information de type (Tacinv ↵Gravatar herbelin2004-12-06
| | | | | | envoie à refine des métas castées avec des métas ?!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6423 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de la coercion vis à vis du but au niveau de RefineGravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6422 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relâchement obligation d'une contrainte de type sur les Hole en position ↵Gravatar herbelin2004-12-06
| | | | | | terminale, pour plus grande généralité de understand_gen_tcc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6421 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mortGravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6420 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de la coercion vis à vis du but au niveau de Refine suite à ↵Gravatar herbelin2004-12-06
| | | | | | changement de CastedOpenConstr en OpenConstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6419 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réparation bug #888 (les tactiques fix et cofix exigent autant de sous-buts ↵Gravatar herbelin2004-12-06
| | | | | | que de fonctions récursives même si l'une de ses fonctions n'a pas de meta); suppression gmm au passage suite commit précédent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6418 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout bug #888Gravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6417 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout bug #889Gravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6416 85f007b7-540e-0410-9357-904b9bb8a0f7
* C'est trop compliqué de mettre à jour les types du metamap en passant sous ↵Gravatar herbelin2004-12-06
| | | | | | les lieurs, plus simple de garder le type avec un cast (cf bug #889) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inutile de réserver les notations à base de '{ }'Gravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6410 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentaireGravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6409 85f007b7-540e-0410-9357-904b9bb8a0f7
* Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des ↵Gravatar herbelin2004-12-06
| | | | | | tactiques d'appliquer une éventuelle coercion vers le but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ affichage nouvelle syntaxeGravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6407 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentaireGravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6405 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug (cf #892)Gravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6403 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6402 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ changements ChoiceFactsGravatar herbelin2004-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6401 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6400 85f007b7-540e-0410-9357-904b9bb8a0f7
* Paramétrisation du domaine des axiomes de choix + ajout description = ↵Gravatar herbelin2004-12-05
| | | | | | choice pour les propriétés décidables vers nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 'set n in * |-'Gravatar herbelin2004-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6398 85f007b7-540e-0410-9357-904b9bb8a0f7
* Failed in 8.0pl1Gravatar herbelin2004-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6397 85f007b7-540e-0410-9357-904b9bb8a0f7
* Orthographe!Gravatar herbelin2004-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6395 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagation du nom des hyps du prédicat de filtrage pour le message ↵Gravatar herbelin2004-12-03
| | | | | | d'erreur elim_arity et réparation dans build_initial_predicate du bug mentionné dans success/Case8.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6394 85f007b7-540e-0410-9357-904b9bb8a0f7
* Was failing in 8.0pl1Gravatar herbelin2004-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6393 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration message d'erreur v8Gravatar herbelin2004-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6391 85f007b7-540e-0410-9357-904b9bb8a0f7
* pp of nested fixpoints (dangling with/for)Gravatar barras2004-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6387 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export pr_intro_patternGravatar herbelin2004-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6385 85f007b7-540e-0410-9357-904b9bb8a0f7
* UserError in reduce_to_*_refGravatar herbelin2004-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6382 85f007b7-540e-0410-9357-904b9bb8a0f7
* Complétion commit précédentGravatar herbelin2004-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6381 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar gregoire2004-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6380 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction 1.138 appliquée à tort à la branche principale au lieu de ↵Gravatar herbelin2004-11-29
| | | | | | V8-0bugfix; retour version 1.137 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6379 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commit précédent erroné; retour version précédenteGravatar herbelin2004-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6377 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression bruit perlGravatar herbelin2004-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-commit version nouvelle syntaxeGravatar herbelin2004-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6370 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ vis à vis de extratacticsGravatar herbelin2004-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6368 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 06:40:39 +0000