aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/logic.ml
Commit message (Expand)AuthorAge
* Merge remote-tracking branch 'github/pr/263' into v8.6Gravatar Maxime Dénès2016-10-03
|\
* | Moving "move" in the new proof engine.Gravatar Hugo Herbelin2016-09-24
| * Tracking careless uses of slow name lookup.Gravatar Pierre-Marie Pédrot2016-09-09
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Removing some compatibility layers in Tactics.Gravatar Pierre-Marie Pédrot2016-05-17
* Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
* | Implementing assert and cut with LetIn rather than using a beta-redex.Gravatar Hugo Herbelin2015-11-07
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\|
| * Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionGravatar Matthieu Sozeau2015-11-04
* | Removing uselessly duplicated function in Evd.Gravatar Pierre-Marie Pédrot2015-09-27
|/
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Removing useless flag of the historical move tactic.Gravatar Pierre-Marie Pédrot2014-11-22
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
* Removing the old rename tactic.Gravatar Pierre-Marie Pédrot2014-11-04
* Removing Convert_concl and Convert_hyp from Logic.Gravatar Hugo Herbelin2014-10-09
* A version of convert_concl and convert_hyp in new proof engine.Gravatar Hugo Herbelin2014-10-09
* A few Global.env removed.Gravatar Hugo Herbelin2014-10-04
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-05
* Revert the two previous commits. I was testing in the wrong branch.Gravatar Pierre-Marie Pédrot2014-09-04
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
* Move UnsatisfiableConstraints to a pretype error.Gravatar Matthieu Sozeau2014-08-22
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
* Fixing "clear" in internal_cut_replace: forbid dependencies in theGravatar Hugo Herbelin2014-06-13
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* Use of "H"-based names for propositional hypotheses obtained byGravatar Hugo Herbelin2014-06-01
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Fix interface for template polymorphism, cleaning up code in all typing algor...Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* 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
* Removing the Change_evar refiner rule.Gravatar Pierre-Marie Pédrot2014-03-31
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
* More sharing in Logic, together with some code cleaning.Gravatar Pierre-Marie Pédrot2014-02-21
* Tracking memory misallocation by trying to improve sharing.Gravatar Pierre-Marie Pédrot2014-02-03
* Algebraized "No such hypothesis" errorsGravatar Pierre-Marie Pédrot2014-01-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-19 08:04:13 +0000