diff options
| author | Maxime Dénès | 2018-12-07 13:38:59 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-16 18:45:32 +0200 |
| commit | 414cfd64702be920c9d96514e3802bc950b5ea0b (patch) | |
| tree | bdc7e8eca2b50da60d1a893124a9c93aea9d1841 /pretyping/pretyping.ml | |
| parent | 4b9119d8090e366ecd2e803ad30a9dd839bc8ec9 (diff) | |
Clean the representation of recursive annotation in Constrexpr
We make clearer which arguments are optional and which are mandatory.
Some of these representations are tricky because of small differences
between Program and Function, which share the same infrastructure.
As a side-effect of this cleanup, Program Fixpoint can now be used with
e.g. {measure (m + n) R}. Previously, parentheses were required around
R.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0f7676cd19..48d981082c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -607,10 +607,10 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env fixpoints ?) *) let possible_indexes = Array.to_list (Array.mapi - (fun i (n,_) -> match n with + (fun i annot -> match annot with | Some n -> [n] | None -> List.map_i (fun i _ -> i) 0 ctxtv.(i)) - vn) + vn) in let fixdecls = (names,ftys,fdefs) in let indexes = esearch_guard ?loc !!env sigma possible_indexes fixdecls in |