diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun.ml | 3 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 8 |
2 files changed, 7 insertions, 4 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 0cacb003d8..1c5eb16218 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -132,6 +132,7 @@ let rec abstract_glob_constr c = function | Constrexpr.LocalRawAssum (idl,k,t)::bl -> List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl (abstract_glob_constr c bl) + | Constrexpr.LocalPattern _::bl -> assert false let interp_casted_constr_with_implicits env sigma impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls @@ -215,6 +216,7 @@ let rec local_binders_length = function | [] -> 0 | Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl | Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl + | Constrexpr.LocalPattern _::bl -> assert false let prepare_body ((name,_,args,types,_),_) rt = let n = local_binders_length args in @@ -861,6 +863,7 @@ let make_graph (f_ref:global_reference) = (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal + | Constrexpr.LocalPattern _ -> assert false ) nal_tas ) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 933e2baee3..814e3a4d5a 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1039,8 +1039,8 @@ ARGUMENT EXTEND cpattern PRINTED BY pr_ssrterm INTERPRETED BY interp_ssrterm GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm - RAW_TYPED AS cpattern RAW_PRINTED BY pr_ssrterm - GLOB_TYPED AS cpattern GLOB_PRINTED BY pr_ssrterm + RAW_PRINTED BY pr_ssrterm + GLOB_PRINTED BY pr_ssrterm | [ "Qed" constr(c) ] -> [ mk_lterm c ] END @@ -1058,8 +1058,8 @@ ARGUMENT EXTEND lcpattern PRINTED BY pr_ssrterm INTERPRETED BY interp_ssrterm GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm - RAW_TYPED AS cpattern RAW_PRINTED BY pr_ssrterm - GLOB_TYPED AS cpattern GLOB_PRINTED BY pr_ssrterm + RAW_PRINTED BY pr_ssrterm + GLOB_PRINTED BY pr_ssrterm | [ "Qed" lconstr(c) ] -> [ mk_lterm c ] END |