| Commit message (Expand) | Author | Age |
* | Cleaning of the new implementation of the tactic monad. | Arnaud Spiwack | 2014-08-04 |
* | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | 2014-08-01 |
* | Removing more tactic compatibility layer. | Pierre-Marie Pédrot | 2014-08-01 |
* | Removing some tactic compatibility layer. | Pierre-Marie Pédrot | 2014-08-01 |
* | Add an option to solve typeclass goals generated by apply which can't be | Matthieu Sozeau | 2014-07-31 |
* | Restore proper order of effects in letin_tac_gen. Fixes CFGV again. | Matthieu Sozeau | 2014-07-03 |
* | Synchronized names from the "as" clause with the skeleton of the | Hugo Herbelin | 2014-06-30 |
* | Small refinement about whether it is tolerated for compatibility that | Hugo Herbelin | 2014-06-28 |
* | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin | 2014-06-28 |
* | Extra check for indirect dependency when abstracting a term which is | Hugo Herbelin | 2014-06-28 |
* | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin | 2014-06-28 |
* | Incorrect folding of evars in let_tac_gen made remember fail to store | Matthieu Sozeau | 2014-06-25 |
* | In exact check, use e_type_of to ensure that universe constraints necessary | Matthieu Sozeau | 2014-06-25 |
* | Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it | Pierre-Marie Pédrot | 2014-06-24 |
* | Clenvtac.res_pf is in the new tactic monad. | Pierre-Marie Pédrot | 2014-06-24 |
* | Removing opens to Clenvtac to track its use more easily. | Pierre-Marie Pédrot | 2014-06-23 |
* | Fix semantics of change p with c to typecheck c at each specific occurrence o... | Matthieu Sozeau | 2014-06-23 |
* | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
* | Check resolution of Metas turned into Evars by pose_all_metas_as_evars | Hugo Herbelin | 2014-06-13 |
* | Passing some tactics to the new monad type. | Pierre-Marie Pédrot | 2014-06-12 |
* | fix handling of side effects in abstract (fixes QArithSternBrocot) | Enrico Tassi | 2014-06-11 |
* | Preserve compatibility on examples such as "intros []." on goals such | Hugo Herbelin | 2014-06-06 |
* | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin | 2014-06-04 |
* | Fixing introduction patterns * and ** when used in a branch so that they do n... | Hugo Herbelin | 2014-05-31 |
* | Upgrade Matthieu's new_revert as the "revert" (a "unit tactic"). | Hugo Herbelin | 2014-05-31 |
* | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | 2014-05-26 |
* | Moving the "specialize" tactic out of the AST. Also removed an obsolete | Pierre-Marie Pédrot | 2014-05-22 |
* | Code cleaning & factorizing functions in Equality. | Pierre-Marie Pédrot | 2014-05-09 |
* | Encapsulating some clausenv uses. This simplifies the control flow of some | Pierre-Marie Pédrot | 2014-05-08 |
* | Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic." | Hugo Herbelin | 2014-05-08 |
* | Avoid "revert" to retype-check the goal, and move it to a "new" tactic. | Hugo Herbelin | 2014-05-08 |
* | Isolating a function "make_abstraction", new name of "letin_abstract", | Hugo Herbelin | 2014-05-08 |
* | Renaming new_induct -> induction; new_destruct -> destruct. | Hugo Herbelin | 2014-05-08 |
* | Little reorganization of generalize tactics code w/o semantic changes. | Hugo Herbelin | 2014-05-08 |
* | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ... | Matthieu Sozeau | 2014-05-08 |
* | Use new tactic combinators in tclABSTRACT, to avoid blowup when using V82.tac... | Matthieu Sozeau | 2014-05-06 |
* | Avoid u+k <= v constraints, don't take the sup of an algebraic universe during | Matthieu Sozeau | 2014-05-06 |
* | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau | 2014-05-06 |
* | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
* | - Fix abstract forgetting about new constraints. | Matthieu Sozeau | 2014-05-06 |
* | - Fix handling of polymorphic inductive elimination schemes. | Matthieu Sozeau | 2014-05-06 |
* | Better hashconsing of levels and universes, working with modules. | Matthieu Sozeau | 2014-05-06 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Rewriting [lapply] tactic in the new monad. | Pierre-Marie Pédrot | 2014-04-27 |
* | Removing useless try-with clauses in Goal.enter variants. | Pierre-Marie Pédrot | 2014-04-25 |
* | Fixing various backtrace recordings. | Pierre-Marie Pédrot | 2014-04-25 |
* | Writing tclABSTRACT in the new monad. In particular the unsafe status is now | Pierre-Marie Pédrot | 2014-04-24 |
* | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot | 2014-04-23 |
* | Removing tactic compatibility layer from Elim. | Pierre-Marie Pédrot | 2014-04-22 |
* | Closing bug #3164 | Julien Forest | 2014-04-04 |