Skip to content

Commit 6a820be

Browse files
MevenBertrandMevenBertrand
committed
rebase on onlytermrel
1 parent 6f979a8 commit 6a820be

File tree

25 files changed

+160
-89
lines changed

25 files changed

+160
-89
lines changed

‎opam‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
opam-version: "2.0"
2-
version: "8.19.dev"
2+
version: "8.20.dev"
33
maintainer: "Meven.Bertrand@univ-nantes.fr"
44
dev-repo: "git+https://github.com/CoqHott/logrel-coq.git"
55
bug-reports: "https://github.com/CoqHott/logrel-coq/issues"
@@ -8,12 +8,14 @@ authors: ["Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
88
"Kenji Maillard <kenji.maillard@inria.fr>"
99
"Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>"
1010
]
11+
homepage: "https://github.com/CoqHott/logrel-coq"
12+
description: "A formalisation of meta-theory for a dependent type system, in Coq"
1113
license: "MIT"
1214
depends: [
1315
"coq" { >= "8.20" & < "8.21~" }
1416
"coq-smpl"
1517
"coq-equations" { >= "1.3" }
16-
"coq-autosubst-ocaml" {>= "1.1"}
18+
# "coq-autosubst-ocaml" {>= "1.1"}
1719
"coq-metacoq-template" {>= "1.3.1+8.19"}
1820
]
1921
build: [

‎theories/Algorithmic/PremisePreserve.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ Section MetaCoqLocallyNameless.
5050
| tProj proj t => to_ident_set t
5151
| tFix mfix idx => to_set (fun d => IdentSet.union (to_ident_set d.(dtype)) (to_ident_set d.(dbody))) mfix
5252
| tCoFix mfix idx => to_set (fun d => IdentSet.union (to_ident_set d.(dtype)) (to_ident_set d.(dbody))) mfix
53-
| tInt _ | tFloat _ | tArray _ _ _ _ => IdentSet.empty
53+
| tInt _ | tFloat _ | tArray _ _ _ _ | tString _ => IdentSet.empty
5454
end.
5555

5656
Definition fresh (i : ident) (s : IdentSet.t) : ident :=

‎theories/Decidability/Functions.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -792,7 +792,7 @@ Section CtxTyping.
792792

793793
Variable conv : (context × term × term) ⇀ exn errors unit.
794794

795-
Equations check_ctx : ∇ (Γ : context), [Sing typing]⇒[exn errors] unit :=
795+
Equations check_ctx : ∇ (Γ : context), [Sing (typing conv)]⇒[exn errors] unit :=
796796
check_ctx ε := ret tt ;
797797
check_ctx (Γ,,A) :=
798798
rec Γ ;;[combined_orec (exn _) _ _ _]

‎theories/Decidability/UntypedFunctions.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -227,7 +227,7 @@ Equations uconv_ne : (term × term) -> M unit :=
227227
| ne_anomaly _ _ => undefined
228228
}.
229229

230-
Equations _uconv : ∇ _ : uconv_state × term × term, Sing wh_red ⇒ exn errors ♯ unit :=
230+
Equations _uconv : ∇ _ : uconv_state × term × term, [Sing wh_red]⇒[exn errors] unit :=
231231
(* | (ty_state,ts) := uconv_ty ts;
232232
| (ty_red_state,ts) := uconv_ty_red ts ; *)
233233
| (tm_state,ts) := uconv_tm ts ;

‎theories/LogicalRelation/Application.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
2-
From LogRel.LogicalRelation Require Import Induction Irrelevance Escape Reflexivity Weakening Neutral Transitivity Reduction NormalRed.
2+
From LogRel.LogicalRelation Require Import Induction Escape Irrelevance Reflexivity Weakening Neutral Transitivity Reduction NormalRed.
33

44
Set Universe Polymorphism.
55

‎theories/LogicalRelation/EqRedRight.v‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
(** * LogRel.EqRedRight: Reducibility of the rhs of a reducible conversion between types. *)
22
From Coq Require Import CRelationClasses.
3-
From LogRel.AutoSubst Require Import core unscoped Ast Extra.
4-
From LogRel Require Import Utils BasicAst Notations Context NormalForms UntypedReduction Weakening GenericTyping LogicalRelation.
3+
From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
54
From LogRel.LogicalRelation Require Import Induction Reflexivity Escape Irrelevance Weakening Transitivity Neutral.
65

76
Set Universe Polymorphism.

‎theories/LogicalRelation/Id.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
2-
From LogRel.LogicalRelation Require Import Induction Irrelevance Weakening Neutral Escape Reflexivity NormalRed Reduction Transitivity Universe.
2+
From LogRel.LogicalRelation Require Import Induction Escape Irrelevance Weakening Neutral Reflexivity NormalRed Reduction Transitivity Universe EqRedRight.
33

44
Set Universe Polymorphism.
55
Set Printing Primitive Projection Parameters.

‎theories/LogicalRelation/InstKripke.v‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
11
(** * LogRel.LogicalRelation.InstKripke: combinators to instantiate Kripke-style quantifications *)
2-
From LogRel.AutoSubst Require Import core unscoped Ast Extra.
3-
From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening
4-
GenericTyping LogicalRelation.
5-
From LogRel.LogicalRelation Require Import Induction Escape Reflexivity Neutral Weakening Irrelevance Application Reduction Transitivity NormalRed EqRedRight.
2+
From Coq Require Import CRelationClasses.
3+
From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
4+
From LogRel.LogicalRelation Require Import Induction Escape Reflexivity Neutral Weakening Irrelevance Application Reduction Transitivity NormalRed EqRedRight.
65

76
Set Universe Polymorphism.
87
Set Printing Primitive Projection Parameters.

‎theories/LogicalRelation/Neutral.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
2-
From LogRel.LogicalRelation Require Import Induction Reflexivity Irrelevance Escape.
2+
From LogRel.LogicalRelation Require Import Induction Reflexivity Irrelevance Escape Transitivity.
33

44
Set Universe Polymorphism.
55

‎theories/LogicalRelation/NormalRed.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
From Coq Require Import CRelationClasses.
22
From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
3-
From LogRel.LogicalRelation Require Import Induction Irrelevance Escape Reflexivity Weakening Neutral Transitivity Reduction.
3+
From LogRel.LogicalRelation Require Import Induction Irrelevance Escape Reflexivity Weakening Neutral Transitivity Reduction EqRedRight.
44

55
Set Universe Polymorphism.
66

0 commit comments

Comments
 (0)