diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checkInductive.ml | 5 | ||||
| -rw-r--r-- | checker/checker.ml | 1 | ||||
| -rw-r--r-- | checker/dune | 11 | ||||
| -rw-r--r-- | checker/values.ml | 2 |
4 files changed, 11 insertions, 8 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 4329b2d743..b681fb876e 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -89,6 +89,9 @@ let eq_recarg a1 a2 = match a1, a2 with let eq_reloc_tbl = Array.equal (fun x y -> Int.equal (fst x) (fst y) && Int.equal (snd x) (snd y)) +let eq_in_context (ctx1, t1) (ctx2, t2) = + Context.Rel.equal Constr.equal ctx1 ctx2 && Constr.equal t1 t2 + let check_packet env mind ind { mind_typename; mind_arity_ctxt; mind_arity; mind_consnames; mind_user_lc; mind_nrealargs; mind_nrealdecls; mind_kelim; mind_nf_lc; @@ -105,7 +108,7 @@ let check_packet env mind ind check "mind_nrealdecls" Int.(equal ind.mind_nrealdecls mind_nrealdecls); check "mind_kelim" (check_kelim ind.mind_kelim mind_kelim); - check "mind_nf_lc" (Array.equal Constr.equal ind.mind_nf_lc mind_nf_lc); + check "mind_nf_lc" (Array.equal eq_in_context ind.mind_nf_lc mind_nf_lc); (* NB: here syntactic equality is not just an optimisation, we also care about the shape of the terms *) diff --git a/checker/checker.ml b/checker/checker.ml index 3c93ef7d36..d3f346d76b 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -273,6 +273,7 @@ let explain_exn = function | IllFormedBranch _ -> str"IllFormedBranch" | Generalization _ -> str"Generalization" | ActualType _ -> str"ActualType" + | IncorrectPrimitive _ -> str"IncorrectPrimitive" | CantApplyBadType ((n,a,b),{uj_val = hd; uj_type = hdty},args) -> let pp_arg i judge = hv 1 (str"arg " ++ int (i+1) ++ str"= " ++ diff --git a/checker/dune b/checker/dune index ee427d26c5..73cbbc8d19 100644 --- a/checker/dune +++ b/checker/dune @@ -3,8 +3,7 @@ ; If we don't pack checker we will have a problem here due to ; duplicate module names in the whole build. (library - (name checklib) - (public_name coq.checklib) + (name coq_checklib) (synopsis "Coq's Standalone Proof Checker") (modules :standard \ coqchk votour) (wrapped true) @@ -15,14 +14,14 @@ (public_name coqchk) (package coq) (modules coqchk) - (flags :standard -open Checklib) - (libraries coq.checklib)) + (flags :standard -open Coq_checklib) + (libraries coq_checklib)) (executable (name votour) (public_name votour) (package coq) (modules votour) - (flags :standard -open Checklib) - (libraries coq.checklib)) + (flags :standard -open Coq_checklib) + (libraries coq_checklib)) diff --git a/checker/values.ml b/checker/values.ml index 66467fa8f5..bcac3014be 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -261,7 +261,7 @@ let v_one_ind = v_tuple "one_inductive_body" Int; Int; List v_sortfam; - Array v_constr; + Array (v_pair v_rctxt v_constr); Array Int; Array Int; v_wfp; |