aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/evar_refiner.ml
Commit message (Collapse)AuthorAge
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
| | | | | | | | | (cas d'un terme sans Rel libre), introduction au passage d'un nouveau type d'evar EvarGoal pour raffinement du message d'erreur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9868 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite modif dans instantiate_pf_com: ajout de test pour l'indice 0, et ↵Gravatar notin2007-04-26
| | | | | | uniformisation des messages d'erreur wrt instantiate git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9798 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de révision 9583 de la v8.1 dans le trunkGravatar notin2007-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9584 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made pretyping a functor over a coercion implementation. Pretyping.Default ↵Gravatar msozeau2006-03-22
| | | | | | | | | | | uses the original Coercion implementation. Updated contributions that called pretyping to use the default impl. Also update subtac using the functor, do some renamings and add interfaces for all files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7682 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
* hiding the meta_map in evar_defsGravatar barras2004-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
* unification encore...Gravatar barras2004-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 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
* bypass w_Define when w_refine-ingGravatar corbinea2004-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5868 85f007b7-540e-0410-9357-904b9bb8a0f7
* updated printing of evar context (may loop ?)Gravatar corbinea2004-06-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5857 85f007b7-540e-0410-9357-904b9bb8a0f7
* more evar stuffGravatar corbinea2004-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7
* effective evar refiningGravatar corbinea2004-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5827 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration du message d'erreur "w_unify"Gravatar clrenard2003-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amelioration du message d'erreur en cas de tentative d'instanciationGravatar clrenard2003-11-15
| | | | | | | avec de mauvaise variables lors de l'unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4923 85f007b7-540e-0410-9357-904b9bb8a0f7
* factorisation et generalisation des clausesGravatar barras2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Instantiate ... inGravatar corbinea2003-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 85f007b7-540e-0410-9357-904b9bb8a0f7
* Option pour rendre les vérifications du refiner optionnelleGravatar herbelin2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3400 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
| | | | | | | | | | | | | | | - Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 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
* backtrack dans l'algo d'unificationGravatar barras2002-04-10
| | | | | | | fichier usage incorrect (libdir et bindir ont disparu) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2629 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
| | | | | | | - coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
* Diverses petites simplications de la machine de preuves.Gravatar clrenard2001-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des stamps et donc des *_constraintsGravatar clrenard2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite de la suppression : enamed_declaration est remplace par evar_map.Gravatar clrenard2001-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2164 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 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
* Suppression du retypage dans w_DeclareGravatar herbelin2001-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1933 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
| | | | | | | ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration de la structure des universGravatar barras2001-03-28
| | | | | | | | elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug dans l'utilisation de l'option debugGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mortGravatar herbelin2000-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1146 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@794 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage canonique :Gravatar herbelin2000-10-18
| | | | | | | | | | | | | | declaration = definition | assumption mode de reference = named | rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifier*constr*typed_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction pour make docGravatar herbelin2000-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
| | | | | | | Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 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 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
* 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
* 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
* MAJ ocaml 2.99 (espaces dans la syntaxe des cast)Gravatar herbelin2000-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@284 85f007b7-540e-0410-9357-904b9bb8a0f7
* rattrapage exceptions autres que UserErrorGravatar filliatr1999-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@254 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 21:00:40 +0000