diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-26 14:24:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-26 14:24:54 +0100 |
| commit | 36c6e9508a42d00686e90441999481354152aaa3 (patch) | |
| tree | 882909be1c393764f13923e059448f3808fa0966 /kernel | |
| parent | b58e8aa6525d45473f88fbea71bab88a2b46c825 (diff) | |
| parent | b1a5fe3686ecd5b03e5c7c2efd95716a8e5270ea (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.ml | 2 | ||||
| -rw-r--r-- | kernel/uGraph.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c5595bbc3..110555011 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -134,7 +134,7 @@ let betazeta_appvect n c v = if Int.equal n 0 then applist (substl env t, stack) else match kind_of_term t, stack with Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl - | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack + | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack | _ -> anomaly (Pp.str "Not enough lambda/let's") in stacklam n [] c (Array.to_list v) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 356cf4da6..ee4231b1f 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -834,8 +834,8 @@ let dump_universes output g = let dump_arc u = function | Canonical {univ=u; lt=lt; le=le} -> let u_str = Level.to_string u in - List.iter (fun v -> output Lt (Level.to_string v) u_str) lt; - List.iter (fun v -> output Le (Level.to_string v) u_str) le + List.iter (fun v -> output Lt u_str (Level.to_string v)) lt; + List.iter (fun v -> output Le u_str (Level.to_string v)) le | Equiv v -> output Eq (Level.to_string u) (Level.to_string v) in |