diff options
| author | Maxime Dénès | 2017-04-28 22:15:06 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-28 22:15:06 +0200 |
| commit | 1c8ed18d5f67d7d5656342584b8dcf8a441cb87f (patch) | |
| tree | ce90c93341c58e82813da8b1a567ce6a3f3ed424 /plugins/funind | |
| parent | 4f742e14441581ece247d33020055f15732f126b (diff) | |
Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."
This reverts commit 7bdfa1a4e46acf11d199a07bfca0bc59381874c3.
Diffstat (limited to 'plugins/funind')
| -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 5056d605dc..d335836dfc 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 - c + ~allow_patvar:false c (* Construct a fixpoint as a Glob_term |