diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | proofs/refiner.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index cdb45ccedc..6043857fa5 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -243,7 +243,7 @@ let apply_to_hyp sign id f = found := true; f sign d tail end else add_named_decl d sign) - sign empty_named_context + sign ~init:empty_named_context in if (not !check) || !found then sign' else error "No such assumption" diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 921238d459..e7b2c78f76 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -57,7 +57,7 @@ let norm_goal sigma gl = Sign.fold_named_context (fun (d,b,ty) sign -> add_named_decl (d, option_app red_fun b, red_fun ty) sign) - empty_named_context gl.evar_hyps; + gl.evar_hyps ~init:empty_named_context; evar_body = gl.evar_body} @@ -799,7 +799,7 @@ let thin_sign osign sign = if Sign.lookup_named id osign = (id,c,ty) then sign else raise Different with Not_found | Different -> add_named_decl d sign) - sign empty_named_context + sign ~init:empty_named_context let rec print_proof sigma osign pf = let {evar_hyps=hyps; evar_concl=cl; |