aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
...
* Suppression des coercions non seulement avant l'affichage des notations mais ...Gravatar herbelin2006-01-04
* Redéclaration de la notation à l'import pour être cohérent avec l'activat...Gravatar herbelin2006-01-03
* Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...Gravatar herbelin2005-12-30
* Ajout booléens; nettoyageGravatar herbelin2005-12-30
* Petite correction nom QuantHypArgType suite suppression traducteurGravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Simplifification de vernac_expr li l'abandon du traducteurGravatar herbelin2005-12-23
* Correction bugs commit précédentGravatar herbelin2005-12-22
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
* Changement des named_contextGravatar gregoire2005-12-02
* Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)Gravatar herbelin2005-11-21
* Correction de la correction du test sur le nombre de parametres d'une projectionGravatar herbelin2005-11-19
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Conséquences nettoyage pretyping.mlGravatar herbelin2005-09-09
* Prise en compte de l'utilisation des notations récursives pour faire une not...Gravatar herbelin2005-06-03
* Adoption du nom canonique global_of_constr pour éviter confusion avec type r...Gravatar herbelin2005-05-20
* Déplacement et export de locate_global (ex-locate_reference) de tacinterp ve...Gravatar herbelin2005-05-20
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Standardisation of function names about global references (especially, renami...Gravatar herbelin2005-02-18
* Bug affichage rawconstrGravatar herbelin2005-02-07
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Pour cible make docGravatar herbelin2005-01-21
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* HUGE COMMITGravatar sacerdot2005-01-03
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-03
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02
* Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...Gravatar herbelin2004-12-25
* Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...Gravatar herbelin2004-12-24
* Mecanisme d'affichage des types (notamment les conclusions des buts) typiquem...Gravatar herbelin2004-12-22
* Restauration type casted_open_constr pour tactique refine car l'unification n...Gravatar herbelin2004-12-09
* Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...Gravatar herbelin2004-12-06
* Message d'erreurGravatar herbelin2004-11-17
* Suppression capture des variables par lieurs non liés dans Notation; simplif...Gravatar herbelin2004-11-17
* Suppression capture des variables par lieurs non liés dans NotationGravatar herbelin2004-11-17
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* Ajout de or-pattern pour le match-with v8Gravatar herbelin2004-09-09
* Interpretation et affichage corrects des notations LetTuple, affichage des no...Gravatar herbelin2004-08-23
* Correction bug #830 : les noms des implicites temporaires étaient inconnus a...Gravatar herbelin2004-08-23
* Apply implicit types to local binders tooGravatar herbelin2004-08-06
* Abstraction vis à vis du type loc pour compatibilité ocaml 3.08Gravatar herbelin2004-07-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* Suppression de Rawterm.loc, branchement sur Util.locGravatar herbelin2004-07-16
* Typo (bug #797)Gravatar herbelin2004-06-27
* Amélioration affichage coercions vers FunclassGravatar herbelin2004-06-02
* pb facto des Fixpoint + erreur avec -dump-glob et LoadGravatar barras2004-04-17