aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2019-12-23Merge PR #11293: Rename files with Class in their name to make their role cle...Hugo Herbelin
2019-12-23Merge PR #11274: [library] [cleanup] Remove code duplication.Pierre-Marie Pédrot
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-12-20Fix handling of recursive notations with custom entriesMaxime Dénès
2019-12-18Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ~s...Pierre-Marie Pédrot
2019-12-16Don't pass (ignored) implicits to interp_mutual_inductive_constrGaëtan Gilbert
2019-12-16Remove variance info from inductive entries, infer in indtypingGaëtan Gilbert
2019-12-16reduce arguments of template_polymorphism_candidateGaëtan Gilbert
2019-12-16comInductive: remove redundant check_evars callsGaëtan Gilbert
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
2019-12-13Use ~strict argument consistently in push_context/push_context_set intfsMatthieu Sozeau
2019-12-10[library] [cleanup] Remove code duplication.Emilio Jesus Gallego Arias
2019-12-10Merge PR #10202: Slightly more robust manual implicit argumentsEmilio Jesus Gallego Arias
2019-12-10Make explicit that users should not observe return values of scheme functions.Pierre-Marie Pédrot
2019-12-10Simplify internal flags in scheme declarations.Pierre-Marie Pédrot
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-12-04Impargs: Using ExplByPos/ExplByName rather than encoding index as an ident.Hugo Herbelin
2019-12-03Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.Emilio Jesus Gallego Arias
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-12-02Merge PR #10575: Clean up deprecationsThéo Zimmermann
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
2019-11-30Actually deprecate `SearchAbout`Maxime Dénès
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-27Remove deprecated commands `AddPath`, `AddRecPath` and `DelPath`Maxime Dénès
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-26indTyping: error instead of anomaly for ill-formed templateGaëtan Gilbert
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-11-25Merge PR #11146: Combine similar arguments when printing Arguments commandHugo Herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-21Merge PR #11103: Grammars: unification fix/cofix between constr/vernac + clea...Emilio Jesus Gallego Arias
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
2019-11-20Combine similar arguments when printing Arguments commandGaëtan Gilbert
2019-11-20make VernacArguments closer to user syntaxGaëtan Gilbert
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing (fixin...charguer
2019-11-19G_constr: Renaming record_fields_instance -> fields_def.Hugo Herbelin
2019-11-19Grammar: mini-factorization between fix/cofix and Fixpoint/CoFixpoint.Hugo Herbelin
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
2019-11-15Merge PR #11079: Rename non-unique local nonterminalsHugo Herbelin
2019-11-14Rename non-unique local nonterminalsJim Fehrle
2019-11-13cleanup unused argument for Classes.do_instance_resolve_TCGaëtan Gilbert
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-11-13don't double parse program attribute for vernacinstanceGaëtan Gilbert
2019-11-12Merge PR #11045: Forbid Include inside sectionsPierre-Marie Pédrot
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-11-11Merge PR #11052: Fix #11048: uncaught destKO in inductive typePierre-Marie Pédrot
2019-11-08Make [Proof_global.closed_proof_output] opaqueGaëtan Gilbert
2019-11-05Fix #11048: uncaught destKO in inductive typeGaëtan Gilbert
2019-11-05Forbid Include inside sectionsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 12:37:31 +0000