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