aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2007-07-16Generalized CAMLP4USE for pp dependenciescorbinea
2007-07-13some more useless constant in const_omegaletouzey
2007-07-13Beginning of a reorganisation of the ml part for romega: letouzey
2007-07-13removing a warning at compilation timejforest
2007-07-12Deletion of contrib/extraction/testletouzey
2007-07-12normalisation (by closure) was not performed under fixpointsbarras
2007-07-12port de r9968: bug avec les ring calculatoiresbarras
2007-07-12An optimization to simplify generated obligations removing unnecessary let-in's.msozeau
2007-07-12Fix bug when adding progs with no obligationsmsozeau
2007-07-12Remove dead modules in Subtac.msozeau
2007-07-12Cleanup, use Util list functions when possiblemsozeau
2007-07-11Slight cleanup of refl_omega.ml : in particular it uses now listletouzey
2007-07-10Big reorganization of romega/ReflOmegaCore.v: towards a modular letouzey
2007-07-09Improvements / Bug fixes for ROmega letouzey
2007-07-06minor bug correction (continuing r 9943)jforest
2007-07-06Adding a syntax for "n-ary" rewrite: letouzey
2007-07-06sequel to commit 9952: forgot to adapt xlate to the new n-ary renameletouzey
2007-07-06extension of the rename tactic: the following is now allowed: letouzey
2007-07-06New intro pattern "@A", which generates a fresh name based on A.glondu
2007-07-05Minor bug correction in Function. Non terminating Function e.g. jforest
2007-07-02Better handling of aliases, add command to solve a particular obligation.msozeau
2007-06-26killing some more non-exhaustive patternsletouzey
2007-06-21Correction de plusieurs bugs de l'export XML (utilisation d'un type deherbelin
2007-06-14Add Solve All Obligations command, fix bug in inequality generation introduce...msozeau
2007-06-09Various Program fixes, multiple pattern matches, aliases. Fix bug in coercion...msozeau
2007-06-07Extension of NArith: Nminus, Nmin, etcletouzey
2007-06-07Unification des types + clause filtrage manquante + uniformisation localeherbelin
2007-05-25Modification of VernacScheme to handle a new scheme: Equality (equality invsiles
2007-05-24fixed (PR#1483)corbinea
2007-05-22Nouvelle stratégie d'unification des types des with-bindings dansherbelin
2007-05-20- Propagation des evars non résolues vers les with_bindings; permet par exempleherbelin
2007-05-17correction de bug dans Function et augmentation de la classe des fonctions su...jforest
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2007-05-06Nouveaux changements autour des implicites (notamment suite àherbelin
2007-04-29Orthographe en passantherbelin
2007-04-29Ajout possibilité d'options à trois mots.herbelin
2007-04-28Ajout de la possibilité de faire référence dans certains cas à un nomherbelin
2007-04-28Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.herbelin
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
2007-04-17Correct implementation of undo in obligations handling code, correct some bug...msozeau
2007-04-16Export de simplest_eapply, utilisé dans la contrib interfacenotin
2007-04-05Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func...jforest
2007-04-02Extension to the general sequence operator (tactical). Now in addition to ...emakarov
2007-03-28Support for implicit formal argument types in Program ; parse types in type s...msozeau
2007-03-26Make multiple patterns work again with Program while simplifying the code.msozeau
2007-03-20Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still a...msozeau
2007-03-20traces Ergofilliatr
2007-03-19Forgot to update to new castmsozeau
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2007-03-16 r11153@tannat: jforest | 2007-03-16 10:25:55 +0100jforest