diff options
| author |  Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> | 2016-02-15 16:22:45 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-06-27 12:31:23 +0200 |
| commit | c6d9d4fb142ef42634be25b60c0995b541e86629 (patch) | |
| tree | e6cd36fc03ae7a79d9b65f08b0295bedc485f855 /plugins | |
| parent | 4d4e2f421c1a4f0339568d3c96ff2459a027aa09 (diff) | |
Adding ability to put any pattern in binders, prefixed by a quote.
Cf CHANGES for details.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 0cacb003d..1c5eb1621 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 ) |