index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
tac2intern.ml
Age
Commit message (
Expand
)
Author
2018-10-17
[build] Add dune file + fix warnings.
Emilio Jesus Gallego Arias
2018-07-23
Merge remote-tracking branch 'origin/pr/54'
Pierre-Marie Pédrot
2018-06-18
Adapt to Coq's PR #7797 (removal of reference).
Maxime Dénès
2018-06-18
Fixing a batch of deprecation warnings.
Pierre-Marie Pédrot
2018-05-25
Renaming smartmap and fold_map according to Coq PR #7177.
Hugo Herbelin
2018-04-19
Allowing formatting break around a printed type.
Hugo Herbelin
2018-03-10
[coq] Adapt to coq/coq#6831.
Emilio Jesus Gallego Arias
2018-02-14
[coq] Adapt to coq/coq#6745
Emilio Jesus Gallego Arias
2017-11-02
Moving pattern type constraints to pattern AST.
Pierre-Marie Pédrot
2017-10-07
Remove unused warnings.
Pierre-Marie Pédrot
2017-09-08
Using a dedicated argument for tactic quotations.
Pierre-Marie Pédrot
2017-09-06
Using higher-order representation for closures.
Pierre-Marie Pédrot
2017-09-04
Implementing the non-strict mode.
Pierre-Marie Pédrot
2017-09-04
Proper anomalies for missing registered primitives.
Pierre-Marie Pédrot
2017-09-03
Uniform handling of locations in the various AST.
Pierre-Marie Pédrot
2017-09-03
Allowing ML objects to return mere tactic expressions.
Pierre-Marie Pédrot
2017-09-03
Allowing complex types in ML objects.
Pierre-Marie Pédrot
2017-09-03
Fix coq/ltac2#16: Passing Ltac2 variables to Ltac1 via $ results in anomalies.
Pierre-Marie Pédrot
2017-09-02
Fix coq/ltac2#12: Error should name which match cases are unhandled.
Pierre-Marie Pédrot
2017-08-31
Fix coq/ltac2#3: Constructor expects n arguments should name which constructo...
Pierre-Marie Pédrot
2017-08-29
Rolling our own generic arguments.
Pierre-Marie Pédrot
2017-08-29
Removing dead code for handling of array litterals.
Pierre-Marie Pédrot
2017-08-28
Fix coq/ltac2#6: Expected and actual types are flipped.
Pierre-Marie Pédrot
2017-08-27
Ensure no confusion with unit in rigid variables.
Pierre-Marie Pédrot
2017-08-27
Proper handling of rigid variables in subtyping.
Pierre-Marie Pédrot
2017-08-27
Introducing rebindable toplevel definitions.
Pierre-Marie Pédrot
2017-08-24
Removing dead code about arrays in the AST.
Pierre-Marie Pédrot
2017-08-24
Rely on quoting for lists instead of hardwiring it in the AST.
Pierre-Marie Pédrot
2017-08-18
Removing dead code.
Pierre-Marie Pédrot
2017-08-07
Fix location of not-unit warning.
Pierre-Marie Pédrot
2017-08-07
Introducing grammar-free tactic notations.
Pierre-Marie Pédrot
2017-08-01
Expanding unification variables in typechecking error messages.
Pierre-Marie Pédrot
2017-07-28
Allowing generic patterns in let-bindings.
Pierre-Marie Pédrot
2017-07-27
Factorizing code for constructors and tuples.
Pierre-Marie Pédrot
2017-07-27
Cleaning up code in internalization.
Pierre-Marie Pédrot
2017-07-26
Do not expand trivial patterns in functions.
Pierre-Marie Pédrot
2017-07-26
Ensuring that inductive constructors are always capitalized.
Pierre-Marie Pédrot
2017-07-26
Fix typo in error message
Pierre-Marie Pédrot
2017-07-26
Better typing errors for function types.
Pierre-Marie Pédrot
2017-07-26
Bugfix: wrong access to non-constant constructor compilation.
Pierre-Marie Pédrot
2017-07-25
Generalizing patterns in fun bindings.
Pierre-Marie Pédrot
2017-07-24
Correctly pushing variables for tuple patterns.
Pierre-Marie Pédrot
2017-07-24
Turning the ltac2 subfolder into a standalone plugin.
Pierre-Marie Pédrot
