aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* 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
* Chgt role 2eme argument AList et implantation affichage motifs recursifs de n...Gravatar herbelin2004-04-08
* Bug sur commit 1.44 dans find_constructor (Not_Found pas rattrape)Gravatar herbelin2004-04-06
* Heuristique pour traduire if-then-else quand le re-typage echoueGravatar herbelin2004-03-30
* Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...Gravatar herbelin2004-03-28
* Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...Gravatar herbelin2004-03-27
* Export compute_arguments_scope pour utilisation local a la construction des i...Gravatar herbelin2004-03-27
* Bug protection array_fold_left2Gravatar herbelin2004-03-19
* Motifs recursifs de notations: prise en compte de l'associativite et des nota...Gravatar herbelin2004-03-17
* Mise en place de motifs récursifs dans Notation; quelques simplifications au...Gravatar herbelin2004-03-17
* correction bug de facto des fix (2e)Gravatar barras2004-03-14
* correction bug de facto des fixGravatar barras2004-03-14
* correction bug de choix de noms courts avec Suresnes/BDDGravatar barras2004-03-14
* bug des points fixes (pb avec la contrib Matrices)Gravatar barras2004-03-12
* Correction d'un defaut dans la globalisation des variables de notationsGravatar herbelin2004-03-12
* Branchement EmptyT, UnitT, IT vers leur equivalent dans SetGravatar herbelin2004-03-11
* correction de bugs des points fixesGravatar barras2004-03-08
* modif des fixpoints pour que si on donne une notation au produit, les pts fix...Gravatar barras2004-03-05
* Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...Gravatar herbelin2004-03-02
* Généralisation du type ltac Identifier en IntroPattern; prise en compte des...Gravatar herbelin2004-03-01