aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Proofview: remove a redundant primitive.Gravatar Arnaud Spiwack2014-10-22
* Proofview: move more functions to the Unsafe module.Gravatar Arnaud Spiwack2014-10-22
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Proofview.mli: no more reference to Goal.goal.Gravatar Arnaud Spiwack2014-10-22
* Proofview: factor init and dependent_init.Gravatar Arnaud Spiwack2014-10-22
* Remove unused functions for side effects.Gravatar Arnaud Spiwack2014-10-22
* Remove the deprecated open-constr based refine.Gravatar Arnaud Spiwack2014-10-22
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
* Remove duplicate code.Gravatar Arnaud Spiwack2014-10-22
* Removing dead code in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
* Small invariants in Rewrite code.Gravatar Pierre-Marie Pédrot2014-10-21
* Lazily check that an argument is dependent when constructing evar clauses.Gravatar Pierre-Marie Pédrot2014-10-21
* Fixing decompose_app_rel in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
* Using new clausenv in rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
* Adding an evar version of the make_clenv function.Gravatar Pierre-Marie Pédrot2014-10-21
* Porting Hugo's fix 98f3abb83a to native compiler.Gravatar Maxime Dénès2014-10-21
* Adapting output tests to the removal of the new token warning and toGravatar Hugo Herbelin2014-10-21
* More precise test for #3459.Gravatar Hugo Herbelin2014-10-21
* Dead code.Gravatar Hugo Herbelin2014-10-21
* Continuing experimental printing of the signature of open evars inGravatar Hugo Herbelin2014-10-21
* Removing re-typecheking from "refine" in no-check mode of the newGravatar Hugo Herbelin2014-10-20
* Fixing a (new) part of bug #2729.Gravatar Hugo Herbelin2014-10-20
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Fixing a bug in the presence of let-in in inductive arity.Gravatar Hugo Herbelin2014-10-20
* Revert "Fixing a loop in proof reconstruction for congruence (#2447)."Gravatar Hugo Herbelin2014-10-17
* Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...Gravatar Hugo Herbelin2014-10-17
* Now printing "now a keyword" only in verbose mode.Gravatar Hugo Herbelin2014-10-17
* When facing problem ?id = ?id' in resolution of return predicate,Gravatar Hugo Herbelin2014-10-17
* Experimental printing of the signature of open evars in Check.Gravatar Hugo Herbelin2014-10-17
* New experimental heuristic printing strategy for evar instances: WeGravatar Hugo Herbelin2014-10-17
* Re-displaying evar instances in debugger.Gravatar Hugo Herbelin2014-10-17
* Fixing a loop in proof reconstruction for congruence (#2447).Gravatar Hugo Herbelin2014-10-17
* Essai où assert_style n'est utilisé que si pas visuellement une équation;Gravatar Hugo Herbelin2014-10-17
* More fallout from elisp renameGravatar Anders Kaseorg2014-10-16
* Relaxing again the test on types of replacements in tactic changeGravatar Hugo Herbelin2014-10-16
* In convert_concl/convert_hyp: nf_enter -> enter.Gravatar Hugo Herbelin2014-10-16
* Revert "Naming main goal "Main""Gravatar Hugo Herbelin2014-10-16
* Refactoring proofview: make the definition of the logic monad polymorphic.Gravatar Arnaud Spiwack2014-10-16
* Refresh to avoid algebraic universes on the right.Gravatar Matthieu Sozeau2014-10-16
* Fix test-suite scripts.Gravatar Matthieu Sozeau2014-10-16
* Bug fixed by Hugo.Gravatar Matthieu Sozeau2014-10-16
* Grab Existential Variables: restore the goal order from v8.4.Gravatar Arnaud Spiwack2014-10-16
* Proofview: cleanup: no more reference to Goal.goal.Gravatar Arnaud Spiwack2014-10-16
* Put evars remaining after a tactic on the shelf.Gravatar Arnaud Spiwack2014-10-16
* Refine: proper scoping of the future goals.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove [advance] from the API.Gravatar Arnaud Spiwack2014-10-16
* Proofview: remove unused [refresh_sigma] compatibility primitive.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove some functions from the compatibility layer.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove most of the API (make [Goal.goal] concrete).Gravatar Arnaud Spiwack2014-10-16
* Make [Goal.goal] be exactly [Evar.t].Gravatar Arnaud Spiwack2014-10-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 21:04:03 +0000