Commits

History for

Commits on Oct 27, 2021

Merge pull request formal-land#196 from pedrotst/grab_existentials
clarus
committedOct 27, 2021

Commits on Oct 15, 2021

Update the documentation links to foobar-land.github.io
clarus
committedOct 15, 2021

Commits on Sep 7, 2021

Documents [@coq_grab_existentials]
pedrotst
committedSep 7, 2021

Commits on Sep 4, 2021

Upgrade a few doc dependencies for security reasons
clarus
committedSep 4, 2021
Add an FAQ page
clarus
committedSep 4, 2021

Commits on Jun 29, 2021

Add fixes to the cookbook
clarus
committedJun 29, 2021
Add more recipes in the cookbook
clarus
committedJun 29, 2021
Add beginning of a cookbook for coq-of-ocaml
clarus
committedJun 29, 2021
Update doc/docs/gadts.md

pedrotst
and
clarus
committedJun 29, 2021
Adds tags attributes to docs
pedrotst
committedJun 29, 2021

Commits on Jun 25, 2021

Documentation for Tagged GADTs
pedrotst
committedJun 25, 2021

Commits on Apr 26, 2021

More explicit link to the main example
clarus
committedApr 26, 2021
Remove the roadmap (because it is outdated)
clarus
committedApr 26, 2021
Add an example page
clarus
committedApr 26, 2021
Add a package-lock file (why was not it there?)
clarus
committedApr 26, 2021

Commits on Apr 13, 2021

Add proofs vs happiness diagram
clarus
committedApr 13, 2021

Commits on Apr 10, 2021

Backquote all the coq-of-ocaml occurences
clarus
committedApr 10, 2021
Small changes to the introduction
clarus
committedApr 10, 2021
Update the introduction
clarus
committedApr 10, 2021
Clean the homepage
clarus
committedApr 10, 2021

Commits on Mar 15, 2021

Upgrade to Merlin 3.4.2
clarus
committedMar 15, 2021

Commits on Feb 19, 2021

Various documentation updates
clarus
committedFeb 19, 2021

Commits on Feb 12, 2021

Add the @coq_type_annotation attribute
clarus
committedFeb 12, 2021

Commits on Feb 11, 2021

Simplify the escaping for name collision, avoiding the use of '__' which generates warning for the extraction
clarus
committedFeb 11, 2021

Commits on Jan 5, 2021

Simplify the header in the generated files
clarus
committedJan 5, 2021

Commits on Dec 17, 2020

Add the attribute @coq_mutual_as_notation to translate mutually recursive functions as notations
clarus
committedDec 17, 2020

Commits on Nov 26, 2020

Add the configuration option 'renaming_type_constructor' to rename the type constructors
clarus
committedNov 26, 2020

Commits on Nov 23, 2020

Add the configuration options 'constant_warning' and 'operator_infix'
clarus
committedNov 23, 2020
Add the configuration option first_class_module_signature_blacklist to ignore signatures
clarus
committedNov 23, 2020

Commits on Oct 28, 2020

Add handling of OCaml's monadic notations
clarus
committedOct 28, 2020

Commits on Oct 26, 2020

Add the attribute @coq_cast to force the cast to a type
clarus
committedOct 26, 2020

Commits on Oct 19, 2020

Rename the attribute @coq_axiom as @coq_axiom_with_reason
clarus
committedOct 19, 2020
Add the attribute @coq_precise_signature to help to distinguish signatures
clarus
committedOct 19, 2020

Commits on Sep 3, 2020

Add the merge_returns configuration option
clarus
committedSep 3, 2020
Add the merge_types configuration option
clarus
committedSep 3, 2020