aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-10-13Deplacement pr_subgoal and co vers Pfeditherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4609 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Ajout d'une fonction de recherche sur les composantes du nom des objetsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4608 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Protection contre les noms de lemmes existant dejaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4607 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Deplacement pr_subgoal and co vers Pfedit; Ajout SearchNamedherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4606 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Deplacement next_global_ident_away dans Termopsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4605 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4604 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11reparation Undo suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4603 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11Uniformisation comportement decompEq pour corriger un bug introduit dans le ↵herbelin
Inversion acceptant le nommage des hypotheses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4602 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11Bug calcul du nom de la premiere equationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4601 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11translate_file etait abusivement positionneherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4600 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11Ajout fnl() dans Aboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4599 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11Logic_TypeSyntax disparuherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4598 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11Death of 'a somewhat cryptic module'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4597 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11Death of 'a somewhat cryptic module'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4596 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11mise a jour nouvelle syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4595 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4594 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Suppression Grammar/Syntaxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4593 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4592 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10nat_scope ouvert par defautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4591 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4590 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10type_scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4589 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Suppression de definitions equivalentesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4588 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Bug undoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4587 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Notation '^'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4586 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4585 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Plus d'Eval Computeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4584 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10MAJ commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4583 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4582 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4581 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4580 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Delimiters N devient 'nat'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4579 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Cablage en dur de inversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4578 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4577 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10show_subgoals dans Pfeditherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4576 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4575 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10MAJ .v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4574 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10pf_get_new_id en provenance de feu wcclausenvherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4573 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Suppression clenv_change_head que seul Wcclausenv utisaitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4572 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Dead of 'a somewhat cryptic module'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4571 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Dead of 'a somewhat cryptic module' (Inv doesn't use applyUsing any longer; ↵herbelin
pf_get_new_id moved to Tacmach) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4570 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Ajout printers pour constr et constr_pattern (sans traduction)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4569 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Unification lemInv et lemInv_inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4568 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10pr_tactic sans traduction; affichage Inversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4567 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Cablage en dur de inversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4566 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4565 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Intégration de la premiere partie de 'hightactics' dans 'tactics' suite à ↵herbelin
cablage en dur de Inversion dans tacexpr.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4564 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Affichage des buts par Pfedit pour utilisation par les tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4563 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Affichage des buts par Pfedit pour utilisation par les tactiques ↵herbelin
(Setoid_replace) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4562 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ↵herbelin
pour utilisation par les tactiques (Setoid_replace) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4561 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Gestion en temps constant de la pile des Unfoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4560 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 13:26:49 +0000