aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2017-10-24Removing dead code which raised questions.Hugo Herbelin
2017-10-20Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Maxime Dénès
2017-10-17[vernac] [state] Cache freeze/unfreezeEmilio Jesus Gallego Arias
2017-10-17[stm] Remove state-handling from Futures.Emilio Jesus Gallego Arias
2017-10-17[stm] Move interpretation state to VernacentriesEmilio Jesus Gallego Arias
2017-10-10Parse [Proof using Type] without translating Type to an id.Gaëtan Gilbert
2017-10-10Use a nice printer for constant names in Suggest Proof Using.Gaëtan Gilbert
2017-10-10Code factorization Vernacentries.interp on VernacProof.Gaëtan Gilbert
2017-10-10[vernac] Remove "Proof using" hacks from parser.Emilio Jesus Gallego Arias
2017-10-10Take Suggest Proof Using outside the kernel.Gaëtan Gilbert
2017-10-10Merge PR #1053: [deps] Move `Discharge` to `interp`Maxime Dénès
2017-10-09Merge PR #1114: Generic handling of nameable objects for pluginsMaxime Dénès
2017-10-09[deps] Move `Discharge` to `interp`Emilio Jesus Gallego Arias
2017-10-09Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...Maxime Dénès
2017-10-06Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ...Maxime Dénès
2017-10-05Merge PR #1081: Mini fix at improving the cannot unify error messageMaxime Dénès
2017-10-05Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...Maxime Dénès
2017-10-05Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).Hugo Herbelin
2017-10-05Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Hugo Herbelin
2017-10-03Implementing a generic mechanism for locating named objects from Coq side.Pierre-Marie Pédrot
2017-10-03Merge PR #1040: Efficient fresh name generationMaxime Dénès
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-26Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Maxime Dénès
2017-09-25BZ#5739, Allow level for leftmost nonterminal for printing-ony NotationsPaul Steckler
2017-09-25Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...Maxime Dénès
2017-09-25Merge PR #1057: Reporting locations in error messages about notation formats.Maxime Dénès
2017-09-23Discharge.ml: cosmetic renaming of some variables.Hugo Herbelin
2017-09-23Fixing #5755 (discharging of inductive types not correct with let-ins).Hugo Herbelin
2017-09-22Himsg: Dropping nf_evars made obsolete by EConstr.Hugo Herbelin
2017-09-22Cannot unify message: improve preventing repeating twice the same message.Hugo Herbelin
2017-09-22Merge PR #1055: Remove STM vernacularsMaxime Dénès
2017-09-20[flags] Flag `open Flags`Emilio Jesus Gallego Arias
2017-09-19Remove STM vernaculars.Maxime Dénès
2017-09-19Don't lose names in UState.universe_context.Gaëtan Gilbert
2017-09-19proof_global: cleanup and comment close_proofMatthieu Sozeau
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-09-18Reporting locations in error messages about notation formats.Hugo Herbelin
2017-09-18Fixing two anomalies in corner cases of the syntax of notation formats.Hugo Herbelin
2017-09-15Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...Maxime Dénès
2017-09-15Merge PR #1051: Using an algebraic type for distinguishing toplevel input fro...Maxime Dénès
2017-09-15Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Maxime Dénès
2017-09-15Merge PR #1037: Parse directly to Sorts.family when appropriate.Maxime Dénès
2017-09-15Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...Maxime Dénès
2017-09-14Using an algebraic type for distinguishing toplevel input from location in file.Hugo Herbelin
2017-09-13A possible fix for BZ#5715 (escape non-utf8 win32 file names).Hugo Herbelin
2017-09-12Fixing bug #5693 (treating empty notation format as any format).Hugo Herbelin
2017-09-12Port is_Set and is_Type to EConstr, as was is_Prop already.Guillaume Melquiond
2017-09-08Parse directly to Sorts.family when appropriate.Gaëtan Gilbert
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 00:47:29 +0000