diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-01-19 02:06:19 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-01-19 02:08:02 +0100 |
| commit | 029854c7f0c10caf0c26b1e3d73ae011c54ac80e (patch) | |
| tree | ee5ca59feaa7ea0c1ea3236ae96944d4b0f9d892 /checker/inductive.ml | |
| parent | 05d5f8b9065b0f5e0349cf3d39dd62ab99f30369 (diff) | |
Fixing checker compilation, which was broken by the following commit:
05d5f8b9065b0f5e0349cf3d39dd62ab99f30369
Diffstat (limited to 'checker/inductive.ml')
| -rw-r--r-- | checker/inductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index c00a6c5dd..1130c5e03 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -295,7 +295,7 @@ let is_correct_arity env c (p,pj) ind specif params = check_allowed_sort (family_of_sort s') specif; false | _, (_,Some _,_ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' u + srec (push_rel d env) (lift 1 pt') ar' | _ -> raise (LocalArity None) in |