aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-10-21Lazily check that an argument is dependent when constructing evar clauses.Pierre-Marie Pédrot
2014-10-21Fixing decompose_app_rel in Rewrite.Pierre-Marie Pédrot
2014-10-21Using new clausenv in rewrite.Pierre-Marie Pédrot
2014-10-21Adding an evar version of the make_clenv function.Pierre-Marie Pédrot
2014-10-21Porting Hugo's fix 98f3abb83a to native compiler.Maxime Dénès
2014-10-21Adapting output tests to the removal of the new token warning and toHugo Herbelin
2014-10-21More precise test for #3459.Hugo Herbelin
2014-10-21Dead code.Hugo Herbelin
2014-10-21Continuing experimental printing of the signature of open evars inHugo Herbelin
2014-10-20Removing re-typecheking from "refine" in no-check mode of the newHugo Herbelin
2014-10-20Fixing a (new) part of bug #2729.Hugo Herbelin
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-10-20Fixing a bug in the presence of let-in in inductive arity.Hugo Herbelin
2014-10-17Revert "Fixing a loop in proof reconstruction for congruence (#2447)."Hugo Herbelin
2014-10-17Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...Hugo Herbelin
2014-10-17Now printing "now a keyword" only in verbose mode.Hugo Herbelin
2014-10-17When facing problem ?id = ?id' in resolution of return predicate,Hugo Herbelin
2014-10-17Experimental printing of the signature of open evars in Check.Hugo Herbelin
2014-10-17New experimental heuristic printing strategy for evar instances: WeHugo Herbelin
2014-10-17Re-displaying evar instances in debugger.Hugo Herbelin
2014-10-17Fixing a loop in proof reconstruction for congruence (#2447).Hugo Herbelin
2014-10-17Essai où assert_style n'est utilisé que si pas visuellement une équation;Hugo Herbelin
2014-10-16More fallout from elisp renameAnders Kaseorg
2014-10-16Relaxing again the test on types of replacements in tactic changeHugo Herbelin
2014-10-16In convert_concl/convert_hyp: nf_enter -> enter.Hugo Herbelin
2014-10-16Revert "Naming main goal "Main""Hugo Herbelin
2014-10-16Refactoring proofview: make the definition of the logic monad polymorphic.Arnaud Spiwack
2014-10-16Refresh to avoid algebraic universes on the right.Matthieu Sozeau
2014-10-16Fix test-suite scripts.Matthieu Sozeau
2014-10-16Bug fixed by Hugo.Matthieu Sozeau
2014-10-16Grab Existential Variables: restore the goal order from v8.4.Arnaud Spiwack
2014-10-16Proofview: cleanup: no more reference to Goal.goal.Arnaud Spiwack
2014-10-16Put evars remaining after a tactic on the shelf.Arnaud Spiwack
2014-10-16Refine: proper scoping of the future goals.Arnaud Spiwack
2014-10-16Goal: remove [advance] from the API.Arnaud Spiwack
2014-10-16Proofview: remove unused [refresh_sigma] compatibility primitive.Arnaud Spiwack
2014-10-16Goal: remove some functions from the compatibility layer.Arnaud Spiwack
2014-10-16Goal: remove most of the API (make [Goal.goal] concrete).Arnaud Spiwack
2014-10-16Make [Goal.goal] be exactly [Evar.t].Arnaud Spiwack
2014-10-16Goal: remove dead code.Arnaud Spiwack
2014-10-16Expose Proofview.Refine.with_type in the API.Arnaud Spiwack
2014-10-16Proofview.Refine: remove the handle type, and simplify the API.Arnaud Spiwack
2014-10-16Move the handling of the principal evar from refine to evd.Arnaud Spiwack
2014-10-16Move the handling a new evars from the [Proofview.Refine] module to [Evd].Arnaud Spiwack
2014-10-16Evd: a few comments to document the increasingly wide internal [evar_map] type.Arnaud Spiwack
2014-10-16Evd: remove/update obsolete comments.Arnaud Spiwack
2014-10-16Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ...Arnaud Spiwack
2014-10-16Proofview: small optimisation/simplification.Arnaud Spiwack
2014-10-16ConstructiveEpsilon: simplify the before_witness type using non-uniform param...Arnaud Spiwack
2014-10-15Adding a timeout to bug #2447.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 12:03:08 +0000