aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Add a flag to control betaiota reduction during unification to maintain backw...Gravatar msozeau2011-04-18
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Applying Tom Prince's patch for build_constant_by_tactic not able toGravatar herbelin2011-04-08
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsGravatar letouzey2011-03-18
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Forgot a use of evars_reset_evd in nf_evars, add an optional argument asGravatar msozeau2011-03-10
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
* Try to fix the behavior of clenv_missing used when declaring hintsGravatar letouzey2011-02-22
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* Started to fix the declarative proof mode (C-zar).Gravatar aspiwack2011-02-10
* Factorize code of rewrite to make way for a new implementation using theGravatar msozeau2011-02-07
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Clenv.connect_clenv without its Evd.foldGravatar letouzey2010-12-15
* Goal: preventively replace an Evd.fold by an equivalent Evd.fold_undefinedGravatar letouzey2010-12-13
* Attempt to preserve casts during a refine, especially VMcastGravatar letouzey2010-12-10
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
* Fix minor typo in error message (Closes: #2408)Gravatar glondu2010-10-25
* Remove open_subgoals field of proof_treeGravatar glondu2010-10-06
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
* In the computation of missing arguments for apply, accept that theGravatar herbelin2010-09-17
* Fix [clenv_missing] to compute a better approximation of missingGravatar msozeau2010-08-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proofGravatar herbelin2010-07-21
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Quick fix for having clenv debug printer working in trunk.Gravatar herbelin2010-06-18
* 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
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
* Fix commentGravatar glondu2010-06-07
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Typo in comment of proof.mlGravatar herbelin2010-05-29
* 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
* Fix: Pfedit.get_current_goal_context when no goal is focused.Gravatar aspiwack2010-05-10
* Removed an evar_merge in clenv_fchain which not only is incorrect butGravatar herbelin2010-05-10
* Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proofGravatar pboutill2010-05-05
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* 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
* Consider OccurCheck a catchable exception.Gravatar msozeau2010-03-08
* New command Declare Reduction <id> := <conv_expr>.Gravatar letouzey2010-01-28
* Errors issued by reduction tactics (e.g. pattern) were not caught by "try".Gravatar herbelin2010-01-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 10:01:52 +0000