aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenv.mli
Commit message (Expand)AuthorAge
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* Tacticals API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
|\|
* | Inlining the only use of Clenv.connect_clenv.Gravatar Pierre-Marie Pédrot2015-11-18
| * Performance fix for destruct.Gravatar Pierre-Marie Pédrot2015-11-17
|/
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Cleaning and documenting Clenv.make_evar_clauseGravatar Pierre-Marie Pédrot2014-10-27
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Lazily check that an argument is dependent when constructing evar clauses.Gravatar Pierre-Marie Pédrot2014-10-21
* Adding an evar version of the make_clenv function.Gravatar Pierre-Marie Pédrot2014-10-21
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Simplifying interface of elimination tactics. They used dummy clausenvs, andGravatar Pierre-Marie Pédrot2014-04-22
* Moving some tactic code to the new engine.Gravatar Pierre-Marie Pédrot2014-03-26
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Removing useless evar-related stuff.Gravatar ppedrot2013-09-25
* Backtrack on unneeded change of interface for pose_metas_as_evars.Gravatar msozeau2013-06-04
* Start documenting new [rewrite_strat] tactic that applies rewritingGravatar msozeau2013-06-04
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Updating headers.Gravatar herbelin2012-08-08
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Cleaning debugging printer relative to new proof engine. InGravatar herbelin2011-06-21
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
* 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