diff options
| author | Pierre-Marie Pédrot | 2018-06-28 18:36:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-25 20:15:18 +0200 |
| commit | 86d08ece4c63e2a42f72ddd3afc51ce04cd1932a (patch) | |
| tree | 314eac7625739d9047b4210e8622695b0007e884 /pretyping/inductiveops.ml | |
| parent | 7cc70b0df61718a946327d5bfb056b140eeb54ba (diff) | |
Fix an algorithmic issue in the vernac guardedness checker.
Calling the O(n) EConstr.to_constr function at every node is a very bad
idea (tm).
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ec0ff73062..1ecd4773ae 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -750,8 +750,11 @@ let type_of_projection_knowing_arg env sigma p c ty = syntactic conditions *) let control_only_guard env sigma c = + let c = Evarutil.nf_evar sigma c in let check_fix_cofix e c = - match kind (EConstr.to_constr sigma c) with + (** [c] has already been normalized upfront *) + let c = EConstr.Unsafe.to_constr c in + match kind c with | CoFix (_,(_,_,_) as cofix) -> Inductive.check_cofix e cofix | Fix (_,(_,_,_) as fix) -> |