diff options
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/funind/indfun.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 99b04898b..8d5b1e782 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -133,7 +133,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 + | Constrexpr.LocalRawPattern _::bl -> assert false let interp_casted_constr_with_implicits env sigma impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls @@ -217,7 +217,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 + | Constrexpr.LocalRawPattern _::bl -> assert false let prepare_body ((name,_,args,types,_),_) rt = let n = local_binders_length args in @@ -871,7 +871,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 + | Constrexpr.LocalRawPattern _ -> assert false ) nal_tas ) |