aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenv.mli
Commit message (Expand)AuthorAge
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* In the computation of missing arguments for apply, accept that theGravatar herbelin2010-09-17
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Fixed bug #2314 (inversion using not checking the correctness of its argumentsGravatar herbelin2010-06-13
* Fix bug #2317: setoid_rewrite ignored binding lists. SlightlyGravatar msozeau2010-06-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* deplacement de clenv vers pretypingGravatar barras2004-09-03
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Suppression clenv_change_head que seul Wcclausenv utisaitGravatar herbelin2003-10-10
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Légère amélioration des messages d'erreur des with-bindings et des RewriteGravatar herbelin2002-12-21
* suite du commit precedentGravatar barras2002-12-19
* Vraie substitutivite de autohintsGravatar coq2002-10-01
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Re-introduction de clenv_constrain_missing_arg utilisé par la contrib LannionGravatar herbelin2002-04-12
* Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.mlGravatar herbelin2002-04-11
* backtrack dans l'algo d'unificationGravatar barras2002-04-10
* transformation des evar en meta preserve la linearite des metasGravatar barras2002-04-03
* - modifs de la condition de garde pour mieux tenir compte des raisonnementsGravatar barras2002-04-02
* backtrack de l'unificationGravatar barras2002-03-21
* encore quelques petites modif de l'unificationGravatar barras2002-03-20
* renommage de fonctionsGravatar barras2002-03-08
* Nouveau Rewrite-in plus economiqueGravatar barras2002-03-04
* Suppression des stamps et donc des *_constraintsGravatar clrenard2001-11-12
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Incompatibilité entre la prise en compte des univers au niveau des tactiques...Gravatar herbelin2001-10-10
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Autoriser Apply avec un but sous forme d'implication ou de quantificationGravatar barras2001-06-29
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* backtrack unification types et deplacement make_clenv_bindingGravatar filliatr2001-03-01
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* - coqmktopGravatar filliatr1999-12-03
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* module WcclausenvGravatar filliatr1999-11-22
* module Clenv (debut)Gravatar filliatr1999-10-20