aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-08-30Merge PR #10714: Solve universe error with SSR 'rewrite !term'Pierre-Marie Pédrot
2019-08-29Solve universe error with SSR 'rewrite !term'Andreas Lynge
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-08-17Delay the computation of frozen evars in legacy unification.Pierre-Marie Pédrot
2019-07-11[proof] Minor cleanup in proof.mlEmilio Jesus Gallego Arias
2019-06-24[proof] Remove last case of optional `?poly` arguments.Emilio Jesus Gallego Arias
2019-06-24[proof] Move initial_euctx to proof_globalEmilio Jesus Gallego Arias
2019-06-24[proof] API Documentation fixes.Emilio Jesus Gallego Arias
2019-06-24[api] Remove `polymorphic` type alias, use labels instead.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
2019-06-24[proof] More uniformity in proof start labels.Emilio Jesus Gallego Arias
2019-06-24[proof] Remove duplicated universe polymorphic from decl_kindsEmilio Jesus Gallego Arias
2019-06-24[proof] Remove redundant universe declaration information.Emilio Jesus Gallego Arias
2019-06-24[lemmas] Reify info for implicits, univ_decls, prepare for rec_thms.Emilio Jesus Gallego Arias
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17[proof] Respond to a comment by Pierre-MarieEmilio Jesus Gallego Arias
2019-06-17[proof] drop parameter from terminator typeEmilio Jesus Gallego Arias
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-06-09[proof] Uniformize Proof_global APIEmilio Jesus Gallego Arias
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-09Merge PR #8726: More robust treatment of the Discharge statusPierre-Marie Pédrot
2019-06-08Merge PR #10263: [proofs] Remove unused API [detected by coverage]Pierre-Marie Pédrot
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-04Rename Proof_global.{pstate -> t}Gaëtan Gilbert
2019-06-04Rename Proof_global.{t -> stack}Gaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-29[proofs] Remove unused API [detected by coverage]Emilio Jesus Gallego Arias
2019-05-26More precise type for Safe_typing export and inlining of private constants.Pierre-Marie Pédrot
2019-05-24Fixing typosJPR
2019-05-23Fixing typos - Part 3JPR
2019-05-15Merge PR #10151: Clean up the API for side-effectsGaëtan Gilbert
2019-05-14Merge PR #8893: Moving evars_of_term from constr to econstrPierre-Marie Pédrot
2019-05-14Abstract away the implementation of side-effects in Safe_typing.Pierre-Marie Pédrot
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
2019-05-13Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.Hugo Herbelin
2019-05-13Merge PR #9887: [api] Remove 8.10 deprecations.Gaëtan Gilbert
2019-05-10Fast-path for reordering of a single closed variable.Pierre-Marie Pédrot
2019-05-10Split the hypothesis conversion check in a conversion + ordering check.Pierre-Marie Pédrot
2019-05-10Logic.convert_hyp now takes an environment as an argument.Pierre-Marie Pédrot
2019-05-10Cleanup of Logic.convert_hyp.Pierre-Marie Pédrot
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-04-24Fix proof bullet error helper (nosuchgoal)Gaëtan Gilbert
2019-04-24[proof] Fix proof bullet error helper which was implemented as a hookEmilio Jesus Gallego Arias
2019-04-05[api] [proofs] Remove dependency of proofs on interp.Emilio Jesus Gallego Arias
2019-04-02Merge PR #9659: Fix #9652: rewrite fails to detect lack of progressEmilio Jesus Gallego Arias
2019-03-27[geninterp] Track polymorphic status in tactic interpretation.Emilio Jesus Gallego Arias
2019-03-27[proof_global] Removal of imperative state.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:34:25 +0000