From d33ced344ba377f0a4003102d77f880fda108fd7 Mon Sep 17 00:00:00 2001
From: glondu
Date: Fri, 24 Dec 2010 23:49:21 +0000
Subject: More {raw => glob} changes for consistency

perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat
tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\
W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s
/glob_terms?/glob_constr/g' **/*.ml*

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/extratactics.ml4 | 4 ++--
 tactics/leminv.mli       | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 6377eafd9e..f774df5dee 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -324,7 +324,7 @@ VERNAC COMMAND EXTEND DeriveInversionClear
   -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
 
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ]
-  -> [ add_inversion_lemma_exn na c (Glob_term.RProp Term.Null) false inv_clear_tac ]
+  -> [ add_inversion_lemma_exn na c (Glob_term.GProp Term.Null) false inv_clear_tac ]
 END
 
 open Term
@@ -335,7 +335,7 @@ VERNAC COMMAND EXTEND DeriveInversion
   -> [ add_inversion_lemma_exn na c s false inv_tac ]
 
 | [ "Derive" "Inversion" ident(na) "with" constr(c) ]
-  -> [ add_inversion_lemma_exn na c (RProp Null) false inv_tac ]
+  -> [ add_inversion_lemma_exn na c (GProp Null) false inv_tac ]
 
 | [ "Derive" "Inversion" ident(na) hyp(id) ]
   -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_tac ]
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 1ac9b4d6fb..233aeba3ab 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -15,5 +15,5 @@ val inversion_lemma_from_goal :
   int -> identifier -> identifier located -> sorts -> bool ->
     (identifier -> tactic) -> unit
 val add_inversion_lemma_exn :
-  identifier -> constr_expr -> rawsort -> bool -> (identifier -> tactic) ->
+  identifier -> constr_expr -> glob_sort -> bool -> (identifier -> tactic) ->
     unit
-- 
cgit v1.2.3