aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/tacred.ml
Commit message (Collapse)AuthorAge
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration des messages d'erreurs de tacred; unfold considère maintenant leGravatar herbelin2006-02-07
| | | | | | | prédicat de filtrage après le terme filtré conformément à l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8003 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage suite à la détection par défaut des variables inutilisées par ↵Gravatar herbelin2005-11-08
| | | | | | ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug invert_names (cf bug #1031)Gravatar herbelin2005-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7490 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adoption du nom canonique global_of_constr pour éviter confusion avec type ↵Gravatar herbelin2005-05-20
| | | | | | reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7048 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation de destApplication en destAppGravatar herbelin2005-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant ↵Gravatar herbelin2005-01-02
| | | | | | dans redexpr.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6544 85f007b7-540e-0410-9357-904b9bb8a0f7
* ExtraRedExpr maintenant sans argument: pas très souple mais au moins ↵Gravatar herbelin2004-12-29
| | | | | | convient pour l'exemple de MapleMode qui lui ne passait pas quand un argument était exigé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6526 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
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
| | | | | | | | | | | | | | | MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans les boxed values .Gravatar gregoire2004-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vérification de la typability de 'pattern'Gravatar herbelin2004-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6226 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un bug de simpl de 1995 + nettoyage (les args de list_fold_left_i etaient ↵Gravatar herbelin2004-09-08
| | | | | | incorrects: 0 au lieu de 1 et lv dans le mauvait sens) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6075 85f007b7-540e-0410-9357-904b9bb8a0f7
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai de suppression de eta dans simpl (cf bug #779)Gravatar herbelin2004-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5853 85f007b7-540e-0410-9357-904b9bb8a0f7
* Terminologie plus intuitive: evaluable -> unfoldableGravatar herbelin2004-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5716 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug #606: mis un message d'erreur plus clairGravatar barras2004-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5653 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug numerotation des occurrences pour 'simpl id at n' (suite)Gravatar herbelin2004-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5338 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug numerotation des occurrences pour 'simpl id at n' (2 protections ↵Gravatar herbelin2004-02-13
| | | | | | maintenant !) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5336 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug (destruct/induction ne savent pas traiter le cas non atomique avec ↵Gravatar herbelin2004-01-27
| | | | | | paramètres) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5252 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage opaqueGravatar herbelin2003-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5133 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des sous-termes imbriqués pour 'simpl ident at nums'Gravatar herbelin2003-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5109 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug introduit avec le 'Simpl f'Gravatar herbelin2003-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'Simpl f'Gravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4966 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout reduce_to_quantified_refGravatar herbelin2003-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4835 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
| | | | | | | | | Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = ↵Gravatar letouzey2003-04-16
| | | | | | list_skipn n l git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3931 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3392 85f007b7-540e-0410-9357-904b9bb8a0f7
* retour en arriere concernant la recherche d'occurence modulo expansion des ↵Gravatar barras2002-10-09
| | | | | | letins, ce qui conduisait a des comportement peu intuitifs. On priviligiera l'utilisation de la tactique Subst. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3110 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction de bugs:Gravatar barras2002-08-16
| | | | | | | | | | | - subst_term_gen ne depliait pas les constantes locales de maniere uniforme - la tactique Simpl ne simplifiait pas les constantes definies dans le contexte de but - la conversion d'un constr vers identificateur ne prenait pas en compte les inductifs et constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise au point de declare_red_exprGravatar herbelin2002-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2736 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finalement un seul constr pour l'instant dans ExtraRedExprGravatar herbelin2002-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2735 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵Gravatar herbelin2002-05-29
| | | | | | commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
| | | | | | | | + Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
* Non dépliage des Fix non réductibles dans HnfGravatar herbelin2001-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2354 85f007b7-540e-0410-9357-904b9bb8a0f7
* compat ocaml 3.03Gravatar filliatr2001-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
* GROS COMMIT:Gravatar barras2001-11-05
| | | | | | | | | | - reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
* TransparentGravatar barras2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage reduce_to_ind et one_step_reduceGravatar herbelin2001-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)Gravatar herbelin2001-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1928 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug SimplGravatar herbelin2001-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1864 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ↵Gravatar herbelin2001-07-21
| | | | | | par le nombre d'args inutiles + vérification dans le noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1862 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-03 14:51:38 +0000