aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Changement 'as notation' en 'where notation'Gravatar herbelin2003-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4632 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles ↵Gravatar herbelin2003-10-14
| | | | | | entrees pour Metasyntax git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4631 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement 'as notation' en 'where notation'; protection 'nat_scope'; ↵Gravatar herbelin2003-10-14
| | | | | | affichage separe des modules importes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4630 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement 'as notation' en 'where notation'; Plus d'uniformite dans la ↵Gravatar herbelin2003-10-14
| | | | | | gestion des implicites d'inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4629 85f007b7-540e-0410-9357-904b9bb8a0f7
* Argument de except, error implicite seulement en v8; Changement 'as ↵Gravatar herbelin2003-10-14
| | | | | | notation' en 'where notation' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4628 85f007b7-540e-0410-9357-904b9bb8a0f7
* Argument de None implicite seulement en v8Gravatar herbelin2003-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4627 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4626 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout projections de tripletGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4625 85f007b7-540e-0410-9357-904b9bb8a0f7
* Admitted rendu independant de Conjecture: plus pratique en mode interactifGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4624 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground update changing left-arrow-arrow rule.Gravatar corbinea2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export is_section_variableGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4622 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug introduit dans start_proof par le commit precedentGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4621 85f007b7-540e-0410-9357-904b9bb8a0f7
* Argument implicite pour None, error, exceptGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4620 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4619 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notations pour l'exponentiationGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enregistrement '^' en v8Gravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4617 85f007b7-540e-0410-9357-904b9bb8a0f7
* CleaningGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ameliration affichage inductifsGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4615 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un Try supplementaire utile pour la compatibilite, car bring_hyps dans ↵Gravatar herbelin2003-10-13
| | | | | | generalizeRewriteIntros peut echouer (typage) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une fonction de recherche sur les composantes du nom des objetsGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4613 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petits bugsGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4612 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement next_global_ident_away dans TermopsGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4611 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une fonction de recherche sur les composantes du nom des objetsGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4610 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement pr_subgoal and co vers PfeditGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4609 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une fonction de recherche sur les composantes du nom des objetsGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre les noms de lemmes existant dejaGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4607 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement pr_subgoal and co vers Pfedit; Ajout SearchNamedGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4606 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement next_global_ident_away dans TermopsGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4605 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-10-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4604 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation Undo suiteGravatar herbelin2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation comportement decompEq pour corriger un bug introduit dans le ↵Gravatar herbelin2003-10-11
| | | | | | Inversion acceptant le nommage des hypotheses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4602 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug calcul du nom de la premiere equationGravatar herbelin2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4601 85f007b7-540e-0410-9357-904b9bb8a0f7
* translate_file etait abusivement positionneGravatar herbelin2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4600 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout fnl() dans AboutGravatar herbelin2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4599 85f007b7-540e-0410-9357-904b9bb8a0f7
* Logic_TypeSyntax disparuGravatar herbelin2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4598 85f007b7-540e-0410-9357-904b9bb8a0f7
* Death of 'a somewhat cryptic module'Gravatar herbelin2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4597 85f007b7-540e-0410-9357-904b9bb8a0f7
* Death of 'a somewhat cryptic module'Gravatar herbelin2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4596 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour nouvelle syntaxeGravatar barras2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4595 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4594 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression Grammar/SyntaxGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4593 85f007b7-540e-0410-9357-904b9bb8a0f7
* identity est equivalent sur Type (sauf sans argument)Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4592 85f007b7-540e-0410-9357-904b9bb8a0f7
* nat_scope ouvert par defautGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4591 85f007b7-540e-0410-9357-904b9bb8a0f7
* identity est equivalent sur Type (sauf sans argument)Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4590 85f007b7-540e-0410-9357-904b9bb8a0f7
* type_scopeGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4589 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de definitions equivalentesGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4588 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug undoGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4587 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notation '^'Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4586 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4585 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus d'Eval ComputeGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4584 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ commentairesGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4583 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 02:04:05 +0000