diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 10:26:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 19:18:41 +0200 |
| commit | 1391955c6635da17b4fb2d7c7b5cec799685e99d (patch) | |
| tree | 347018f490760b930c477096c08d97592a945915 /kernel/inductive.ml | |
| parent | 2aaced1d2486deb901ea0a5b134ef28273dda67f (diff) | |
Unused variables reported by OCaml.
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 00d14a25e..cf4177c50 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -153,7 +153,7 @@ let remember_subst u subst = (* Propagate the new levels in the signature *) let rec make_subst env = let rec make subst = function - | (_,Some _,_ as t)::sign, exp, args -> + | (_,Some _,_)::sign, exp, args -> make subst (sign, exp, args) | d::sign, None::exp, args -> let args = match args with _::args -> args | [] -> [] in @@ -166,7 +166,7 @@ let rec make_subst env = (* a useless extra constraint *) let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in make (cons_subst u s subst) (sign, exp, args) - | (na,None,t as d)::sign, Some u::exp, [] -> + | (na,None,t)::sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) (* template, it is identity substitution otherwise (ie. when u is *) |