From 865d3a274dc618a4eff13b309109aa559077a933 Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 12 Nov 2001 12:38:08 +0000
Subject: Suites modifs du noyau. Univ devient purement fonctionnel.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.ml   | 2 +-
 proofs/refiner.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'proofs')

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; 
-- 
cgit v1.2.3