aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* 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
* MAJGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4582 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4581 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delimiters N devient 'nat'Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4579 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cablage en dur de inversionGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4578 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4577 85f007b7-540e-0410-9357-904b9bb8a0f7
* show_subgoals dans PfeditGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4576 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4575 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ .v8Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4574 85f007b7-540e-0410-9357-904b9bb8a0f7
* pf_get_new_id en provenance de feu wcclausenvGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4573 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-22 23:26:50 +0000