From 2bdcd093b357adb2185518dabbafd1a0b9279044 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Tue, 27 Mar 2012 07:41:19 +0200
Subject: Imported Upstream version 8.3.pl4

---
 plugins/funind/recdef.ml             | 5 +++--
 plugins/romega/ReflOmegaCore.v       | 2 +-
 plugins/subtac/subtac_obligations.ml | 4 ++--
 3 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 83868da9..934bf683 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: recdef.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: recdef.ml 15069 2012-03-20 14:06:07Z herbelin $ *)
 
 open Term
 open Termops
@@ -51,7 +51,8 @@ open Genarg
 
 
 let compute_renamed_type gls c =
-  rename_bound_vars_as_displayed [] (pf_type_of gls c)
+  rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
+    (pf_type_of gls c)
 
 let qed () = Lemmas.save_named true
 let defined () = Lemmas.save_named false
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index c82abfc8..04eac3a8 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -872,7 +872,7 @@ Arguments Scope Tint [Int_scope].
 Arguments Scope Tplus [romega_scope romega_scope].
 Arguments Scope Tmult [romega_scope romega_scope].
 Arguments Scope Tminus [romega_scope romega_scope].
-Arguments Scope Topp [romega_scope romega_scope].
+Arguments Scope Topp [romega_scope].
 
 Infix "+" := Tplus : romega_scope.
 Infix "*" := Tmult : romega_scope.
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index d3a63410..80e712e5 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -485,8 +485,8 @@ and solve_obligation_by_tac prg obls i tac =
 	      true
 	  else false
 	with
-	| Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
-	| Stdpp.Exc_located(_, Refiner.FailError (_, s))
+	| Compat.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
+	| Compat.Exc_located(_, Refiner.FailError (_, s))
 	| Refiner.FailError (_, s) ->
 	    user_err_loc (fst obl.obl_source, "solve_obligation", Lazy.force s)
 	| e -> false
-- 
cgit v1.2.3