aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refiner.ml
Commit message (Expand)AuthorAge
...
* Proof_type: rule now degenerates to prim_ruleGravatar letouzey2012-10-06
* Clean-up : no more Proof_type.proof_treeGravatar letouzey2012-10-06
* Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxGravatar letouzey2012-10-06
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Use the library function List.substract in prev commitGravatar letouzey2012-10-02
* Added a new tactical infoH tac, that displays the names of hypothesis created...Gravatar courtieu2012-10-01
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* info_trivial, info_auto, info_eauto, and debug (trivial|auto)Gravatar letouzey2012-03-30
* Noise for nothingGravatar pboutill2012-03-02
* A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsGravatar letouzey2011-03-18
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Fix commentGravatar glondu2010-06-07
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Attached evar source to the evar_info and add location to tclWITHHOLES errorsGravatar herbelin2009-12-22
* In "progress", extending the set of evars w/o solving an existing one isGravatar herbelin2009-12-21
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* pushed evar reduction in kernelGravatar barras2009-02-06
* Really compare evar maps in progress, due to merging in apply and otherGravatar msozeau2009-01-23
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* - Rebranchement backtrack du langage déclaratif dans CoqideGravatar herbelin2008-07-18
* fixed catch_failerror + improved progress check + fixed repeat (repeat simpl ...Gravatar barras2008-05-29
* Move exception-handling code for catching tactics failure Gravatar msozeau2008-05-01
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Adding the tactic "instantiate" (without argument), to force theGravatar glondu2007-12-07
* Extension to the general sequence operator (tactical). Now in addition to ...Gravatar emakarov2007-04-02
* Correction du bug #1315:Gravatar notin2007-01-22
* bug #1194: normalisation evars a la sortie de focusGravatar barras2006-10-23
* affichage des ... dans les scriptsGravatar barras2006-10-16
* revision de la semantique de rewrite ... in <clause>. details dans la docGravatar letouzey2006-10-05
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* replacing whd_betaiotaevar_preserving_vm_cast Gravatar jforest2006-04-14
* Correction bug #842 (rename d'une hyp du contexte)Gravatar herbelin2006-03-01
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* changement d'egalite pour le named_context_valGravatar gregoire2005-12-05
* Changement des named_contextGravatar gregoire2005-12-02
* Confusion assert/error détectée par nouveau warning X de ocaml 3.09Gravatar herbelin2005-11-04