diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-26 12:15:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-31 02:04:09 +0200 |
| commit | 5dd98189c6554733fe4e22401e1637330cc8a30a (patch) | |
| tree | bc580d37a6d3d20b99c36af84913b7f895f79502 /plugins/funind/indfun.ml | |
| parent | bcc9165aec1a80d563d7060ef127ad022e9ed008 (diff) | |
Renaming allow_patvar flag of intern_gen into pattern_mode.
This highlights that this is a binary mode changing the interpretation
of "?x" rather than additionally allowing patvar.
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 74c0eb4cc..72d29f5e0 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -142,7 +142,7 @@ let rec abstract_glob_constr c = function let interp_casted_constr_with_implicits env sigma impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls - ~allow_patvar:false c + c (* Construct a fixpoint as a Glob_term |