Pierre-Marie Pédrot ppedrot
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/usr/bin/env ocaml | |
| #use "topfind";; | |
| #require "str";; | |
| (* This is a quick-and-dirty script to adapt Rocq developments to the removal of | |
| the implicit call to auto with * in the intuition tactic. | |
| How to use: | |
| - Run your build with the intuition warning set on Rocq <= 9.1 and pipe the |
ppedrot
/ gist:d0ed162c415c4abceef662ef675477f9
Last active
August 12, 2025 22:21
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,+fragile-hint-constr,unsupported-attributes" "-w" "-notation-overridden,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src" "Crypto" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Coqprime" "Coqprime" "-Q" "/github/workspace/build |
ppedrot
/ RefMan-gal.tex
Created
July 18, 2022 15:41
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| \chapter{The {\sf Gallina} specification language}\label{Gallina}\index{Gallina} | |
| \section{Lexical conventions}\label{lexical}\index{Lexical conventions} | |
| \paragraph{Blanks} | |
| Space, newline and horizontal tabulation are considered as blanks. | |
| Blanks are ignored but they separate tokens. | |
| \paragraph{Comments} |
ppedrot
/ gist:a68529fc3ed73b0392064ce707280e02
Created
July 18, 2022 15:15
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| * | |
| * gallina May 20 1994 (Jean-Christophe Filliatre) | |
| * | |
| SYNOPSIS | |
| gallina [-] [-stdout] file1 file2 ... | |
| DESCRIPTION |
ppedrot
/ gist:d537b6f4c0ad73554d3dd993731dc5a8
Created
October 15, 2019 18:47
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Set Primitive Projections. | |
| Set Universe Polymorphism. | |
| Set Polymorphic Inductive Cumulativity. | |
| Inductive seq {A : Type} (x : A) : A -> SProp := srefl : seq x x. | |
| Notation "x ≡ y" := (seq x y) (at level 70). | |
| Lemma J_seq : forall (A : Type) (x : A) (P : forall y, x ≡ y -> Type), | |
| P x (srefl _) -> forall y e, P y e. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| CoInductive stream R := | |
| cons : nat -> stream R + R -> stream R. | |
| Definition collapse {L R S T} | |
| (f: L -> S) | |
| (r : S -> T) | |
| (ts: S + (L + R)) : T + R := | |
| match ts with | |
| | inl t => inl (r t) | |
| | inr (inl t) => inl (r (f t)) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| [pview] ow: 082; nw: 082; or:{x:000; y:000; w:000; h000}; nr:{x:695; y:106; w:660; h273} | |
| [mview] ow: 081; nw: 081; or:{x:000; y:000; w:000; h000}; nr:{x:000; y:000; w:000; h000} | |
| [pview] ow: 082; nw: 082; or:{x:695; y:106; w:660; h273}; nr:{x:000; y:000; w:000; h000} | |
| [pview] ow: 080; nw: 080; or:{x:000; y:000; w:000; h000}; nr:{x:695; y:106; w:641; h273} | |
| [mview] ow: 081; nw: 081; or:{x:000; y:000; w:000; h000}; nr:{x:000; y:000; w:000; h000} | |
| [pview] ow: 080; nw: 080; or:{x:695; y:106; w:641; h273}; nr:{x:000; y:000; w:000; h000} | |
| [mview] ow: 081; nw: 081; or:{x:000; y:000; w:000; h000}; nr:{x:000; y:000; w:000; h000} | |
| [pview] ow: 080; nw: 080; or:{x:000; y:000; w:000; h000}; nr:{x:000; y:000; w:000; h000} | |
| [mview] ow: 081; nw: 081; or:{x:000; y:000; w:000; h000}; nr:{x:000; y:000; w:000; h000} | |
| [pview] ow: 080; nw: 080; or:{x:000; y:000; w:000; h000}; nr:{x:000; y:000; w:000; h000} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import Coq.Lists.List. | |
| Require Import ExtLib.Data.HList. | |
| Require Import ExtLib.Data.Member. | |
| Set Implicit Arguments. | |
| Set Strict Implicit. | |
| Arguments MZ {_ _ _}. | |
| Arguments MN {_ _ _ _} _. |