diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-23 18:34:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-23 18:46:27 +0200 |
| commit | 89eaab788fafcadaf5fe5fca8100bddd54675395 (patch) | |
| tree | 161a4f7d4d9c10edc22c03cbfc6378ff2bca0669 | |
| parent | 20eb7fed88ec3154721e34b549e39c0b5cefba23 (diff) | |
Fixing order of declarations in the function which compacts variables
of same type in a context.
| -rw-r--r-- | pretyping/termops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index a1f1f52ff..ee60f60c0 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -948,7 +948,7 @@ let compact_named_context sign = if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2 then (i1::l2,c2,t2)::q else ([i1],c1,t1)::l - in Context.fold_named_context_reverse compact ~init:[] sign + in List.rev (Context.fold_named_context_reverse compact ~init:[] sign) let clear_named_body id env = let aux _ = function |