aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/logic.ml
Commit message (Expand)AuthorAge
...
* 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
* Useless array to list conversions in proof/logic.ml.Gravatar ppedrot2013-10-28
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Replacing lists by sets in clear tactic.Gravatar ppedrot2013-08-25
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Getting rid of LtacLocated exception transformer.Gravatar ppedrot2013-05-28
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 16:30:59 +0000