From 6f60984128d38d1166000223f369fdeb1c6af1a3 Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 23 Dec 2010 18:51:08 +0000
Subject: Rename rawterm.ml into glob_term.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/firstorder/instances.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 24ec234847..881850365a 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -12,7 +12,7 @@ open Unify
 open Rules
 open Util
 open Term
-open Rawterm
+open Glob_term
 open Tacmach
 open Tactics
 open Tacticals
@@ -179,12 +179,12 @@ let right_instance_tac inst continue seq=
 	[tclTHENLIST
 	   [introf;
 	    (fun gls->
-	       split (Rawterm.ImplicitBindings
+	       split (Glob_term.ImplicitBindings
 			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
 	 tclTRY assumption]
     | Real ((0,t),_) ->
-	(tclTHEN (split (Rawterm.ImplicitBindings [t]))
+	(tclTHEN (split (Glob_term.ImplicitBindings [t]))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
 	tclFAIL 0 (Pp.str "not implemented ... yet")
-- 
cgit v1.2.3