aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr>2016-02-15 16:22:45 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-06-27 12:31:23 +0200
commitc6d9d4fb142ef42634be25b60c0995b541e86629 (patch)
treee6cd36fc03ae7a79d9b65f08b0295bedc485f855 /toplevel
parent4d4e2f421c1a4f0339568d3c96ff2459a027aa09 (diff)
Adding ability to put any pattern in binders, prefixed by a quote.
Cf CHANGES for details.
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/command.ml1
-rw-r--r--toplevel/record.ml3
2 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5041d78a3..1fda5b9f7 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -548,6 +548,7 @@ let check_param = function
| LocalRawDef (na, _) -> check_named na
| LocalRawAssum (nas, Default _, _) -> List.iter check_named nas
| LocalRawAssum (nas, Generalized _, _) -> ()
+| LocalPattern _ -> assert false
let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
check_all_names_different indl;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c9b46983e..fe6ed55a7 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -107,7 +107,8 @@ let typecheck_params_and_fields def id pl t ps nots fs =
in
List.iter
(function LocalRawDef (b, _) -> error default_binder_kind b
- | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps
+ | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls
+ | LocalPattern _ -> assert false) ps
in
let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
let t', template = match t with