From c6d9d4fb142ef42634be25b60c0995b541e86629 Mon Sep 17 00:00:00 2001 From: Daniel de Rauglaudre Date: Mon, 15 Feb 2016 16:22:45 +0100 Subject: Adding ability to put any pattern in binders, prefixed by a quote. Cf CHANGES for details. --- toplevel/command.ml | 1 + toplevel/record.ml | 3 ++- 2 files changed, 3 insertions(+), 1 deletion(-) (limited to 'toplevel') 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 -- cgit v1.2.3