aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/evar_refiner.mli
Commit message (Expand)AuthorAge
* Extruding the code for the Existential command from Proofview.Gravatar Pierre-Marie Pédrot2016-03-20
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Updating headers.Gravatar herbelin2012-08-08
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* 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
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* 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
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* Nouvelle en-têteGravatar herbelin2004-07-16
* more evar stuffGravatar corbinea2004-06-28
* effective evar refiningGravatar corbinea2004-06-26
* factorisation et generalisation des clausesGravatar barras2003-11-13
* petits changements de syntaxeGravatar barras2003-11-12
* Added Instantiate ... inGravatar corbinea2003-11-06
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
* Option pour rendre les vérifications du refiner optionnelleGravatar herbelin2002-12-09
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* backtrack dans l'algo d'unificationGravatar barras2002-04-10
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* reparation de make doc (ocamlweb & _)Gravatar letouzey2001-12-19
* Diverses petites simplications de la machine de preuves.Gravatar clrenard2001-11-19
* Suppression des stamps et donc des *_constraintsGravatar clrenard2001-11-12
* Suite de la suppression : enamed_declaration est remplace par evar_map.Gravatar clrenard2001-11-06
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* Suppression du retypage dans w_DeclareGravatar herbelin2001-09-09
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* DocumentationGravatar herbelin2000-12-18
* 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
* Renommage canonique :Gravatar herbelin2000-10-18
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* modifs pour premiere edition de liensGravatar filliatr1999-12-02