aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* RienGravatar herbelin2000-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@522 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifs de presentation.Gravatar delahaye2000-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@520 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> ↵Gravatar filliatr2000-06-21
| | | | | | .vo plus petits git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@514 85f007b7-540e-0410-9357-904b9bb8a0f7
* portage EAuto et RingGravatar filliatr2000-06-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@513 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mortGravatar herbelin2000-06-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@507 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait des lam_and_pop and co (2ème - bug)Gravatar herbelin2000-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@499 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait des lam_and_pop and coGravatar herbelin2000-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@498 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@488 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de GenericGravatar herbelin2000-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@480 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de save_thm and co de PFedit vers CommandGravatar herbelin2000-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@477 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug stupide d'ordre d'évaluationGravatar herbelin2000-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@473 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsGravatar herbelin2000-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@464 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement nommage des hypothèsesGravatar herbelin2000-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@461 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour comportement de la version précédenteGravatar herbelin2000-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@456 85f007b7-540e-0410-9357-904b9bb8a0f7
* bugsGravatar herbelin2000-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@453 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression ligne etrangeGravatar herbelin2000-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@452 85f007b7-540e-0410-9357-904b9bb8a0f7
* ciseauxGravatar herbelin2000-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@449 85f007b7-540e-0410-9357-904b9bb8a0f7
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@447 85f007b7-540e-0410-9357-904b9bb8a0f7
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@442 85f007b7-540e-0410-9357-904b9bb8a0f7
* NettoyageGravatar herbelin2000-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@434 85f007b7-540e-0410-9357-904b9bb8a0f7
* RienGravatar herbelin2000-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@432 85f007b7-540e-0410-9357-904b9bb8a0f7
* Achèvement nettoyage Pfedit; ajout intros_replacingGravatar herbelin2000-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@423 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration de leminvGravatar herbelin2000-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@422 85f007b7-540e-0410-9357-904b9bb8a0f7
* les erreursGravatar herbelin2000-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@417 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)Gravatar herbelin2000-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@416 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation du bug d'interpretation d'AbstractGravatar delahaye2000-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@409 85f007b7-540e-0410-9357-904b9bb8a0f7
* diverses modifs pour ocamlwebGravatar filliatr2000-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@408 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@407 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout get_referenceGravatar herbelin2000-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@404 85f007b7-540e-0410-9357-904b9bb8a0f7
* Encapsulage de PatternMatchingFailure par un 'error' pour que l'echec de ↵Gravatar herbelin2000-05-03
| | | | | | conclPattern soit rattrapable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@403 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
* DiversGravatar herbelin2000-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@397 85f007b7-540e-0410-9357-904b9bb8a0f7
* Problème avec motif du second-ordreGravatar herbelin2000-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@395 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite intégration de constr_patternGravatar herbelin2000-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@393 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration progressiveGravatar herbelin2000-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@390 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptés pour le type constr_pattern et les nouvelles fonctions de filtrageGravatar herbelin2000-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@389 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
| | | | | | | | | Découpage de tactics/pattern en proofs/pattern et tactics/hipattern Renommage des fonctions somatch and co dans Pattern et Tacticals Divers extensions pour utiliser les constr_pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
| | | | | | | | | Découpage de tactics/pattern en proofs/pattern et tactics/hipattern Renommage des fonctions somatch and co dans Pattern et Tacticals Divers extensions pour utiliser les constr_pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@383 85f007b7-540e-0410-9357-904b9bb8a0f7
* Decoupage de tactics/pattern en proofs/pattern et tactics/hipatternGravatar herbelin2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@382 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de représentation du contexte des réf dans rawconstr et patternGravatar herbelin2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@377 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@368 85f007b7-540e-0410-9357-904b9bb8a0f7
* NettoyageGravatar herbelin2000-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@362 85f007b7-540e-0410-9357-904b9bb8a0f7
* erreurs lexicales dans les patterns (manquait des espaces)Gravatar filliatr2000-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@359 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en ↵Gravatar herbelin2000-03-28
| | | | | | {pf_,}interp_constr* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@357 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inversion (pas termine)Gravatar filliatr2000-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@355 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 20:06:18 +0000