diff options
| author | Gaëtan Gilbert | 2018-11-05 14:20:47 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-05 14:20:47 +0100 |
| commit | afc3e334c02cbbbe395387ff7110a296dce6c9f6 (patch) | |
| tree | 426b3dc276987c08fb23f4a58d7687735ede9016 | |
| parent | ebc815989728991850080da0e3033cfabecbb759 (diff) | |
| parent | 86d08ece4c63e2a42f72ddd3afc51ce04cd1932a (diff) | |
Merge PR #7952: Fix an algorithmic issue in the vernac guardedness checker.
| -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 ea222397a8..14358dd02a 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -746,8 +746,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) -> |