diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-02-02 10:18:48 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 12:17:34 +0100 |
| commit | d91a0c27402f0f19a30147bb9d87387ca2a91fd0 (patch) | |
| tree | b0ea13cb3186f8a405b3980c11571b19cc81f7aa /plugins/funind/indfun.ml | |
| parent | 2189505b6e50c9a9aa8e9d520c05461e59f18d04 (diff) | |
"Standardizing" the name LocalPatten into LocalRawPattern.
Diffstat (limited to 'plugins/funind/indfun.ml')
| -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 ) |