| Commit message (Expand) | Author | Age |
* | Applying Tom Prince's patch for build_constant_by_tactic not able to | herbelin | 2011-04-08 |
* | Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks | letouzey | 2011-04-03 |
* | A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds | letouzey | 2011-03-18 |
* | - Add modulo_delta_types flag for unification to allow full | msozeau | 2011-03-13 |
* | Forgot a use of evars_reset_evd in nf_evars, add an optional argument as | msozeau | 2011-03-10 |
* | Reverted commit r13893 about propagation of more informative | herbelin | 2011-03-07 |
* | Added propagation of evars unification failure reasons for better | herbelin | 2011-03-07 |
* | Try to fix the behavior of clenv_missing used when declaring hints | letouzey | 2011-02-22 |
* | - Use transparency information all the way through unification and | msozeau | 2011-02-17 |
* | Started to fix the declarative proof mode (C-zar). | aspiwack | 2011-02-10 |
* | Factorize code of rewrite to make way for a new implementation using the | msozeau | 2011-02-07 |
* | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey | 2011-01-28 |
* | More {raw => glob} changes for consistency | glondu | 2010-12-24 |
* | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |
* | Change of nomenclature: rawconstr -> glob_constr | glondu | 2010-12-23 |
* | Clenv.connect_clenv without its Evd.fold | letouzey | 2010-12-15 |
* | Goal: preventively replace an Evd.fold by an equivalent Evd.fold_undefined | letouzey | 2010-12-13 |
* | Attempt to preserve casts during a refine, especially VMcast | letouzey | 2010-12-10 |
* | Delayed the evar normalization in error messages to the last minute | herbelin | 2010-11-07 |
* | Fix minor typo in error message (Closes: #2408) | glondu | 2010-10-25 |
* | Remove open_subgoals field of proof_tree | glondu | 2010-10-06 |
* | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
* | Added eta-expansion in kernel, type inference and tactic unification, | herbelin | 2010-09-20 |
* | In the computation of missing arguments for apply, accept that the | herbelin | 2010-09-17 |
* | Fix [clenv_missing] to compute a better approximation of missing | msozeau | 2010-08-02 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proof | herbelin | 2010-07-21 |
* | New script dev/tools/change-header to automatically update Coq files headers. | herbelin | 2010-06-22 |
* | Quick fix for having clenv debug printer working in trunk. | herbelin | 2010-06-18 |
* | Fixed bug #2314 (inversion using not checking the correctness of its arguments | herbelin | 2010-06-13 |
* | Fix bug #2317: setoid_rewrite ignored binding lists. Slightly | msozeau | 2010-06-09 |
* | Automatic introduction of names given before ":" in Lemma's and | herbelin | 2010-06-09 |
* | Fix comment | glondu | 2010-06-07 |
* | Added support for Ltac-matching terms with variables bound in the pattern | herbelin | 2010-06-06 |
* | Typo in comment of proof.ml | herbelin | 2010-05-29 |
* | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey | 2010-05-19 |
* | Improved the efficiency of evars traverals thanks to a split of | herbelin | 2010-05-13 |
* | Fix: Pfedit.get_current_goal_context when no goal is focused. | aspiwack | 2010-05-10 |
* | Removed an evar_merge in clenv_fchain which not only is incorrect but | herbelin | 2010-05-10 |
* | Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof | pboutill | 2010-05-05 |
* | Various minor improvements of comments in mli for ocamldoc | letouzey | 2010-04-29 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill | 2010-04-29 |
* | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack | 2010-04-22 |
* | Consider OccurCheck a catchable exception. | msozeau | 2010-03-08 |
* | New command Declare Reduction <id> := <conv_expr>. | letouzey | 2010-01-28 |
* | Errors issued by reduction tactics (e.g. pattern) were not caught by "try". | herbelin | 2010-01-04 |
* | Fixing bug #2146 (broken selection of occurrences in "change"). | herbelin | 2009-12-30 |
* | In "simpl c" and "change c with d", c can be a pattern. | herbelin | 2009-12-24 |
* | Opened the possibility to type Ltac patterns but it is not fully functional yet | herbelin | 2009-12-24 |