diff options
| author | glondu | 2010-12-23 18:51:08 +0000 |
|---|---|---|
| committer | glondu | 2010-12-23 18:51:08 +0000 |
| commit | 6f60984128d38d1166000223f369fdeb1c6af1a3 (patch) | |
| tree | c2a5d166349ef6d643ce8a76b7fd3f84ee9f6cb9 /plugins/decl_mode/decl_interp.ml | |
| parent | 8f9461509338a3ebba46faaad3116c4e44135423 (diff) | |
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
Diffstat (limited to 'plugins/decl_mode/decl_interp.ml')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index d16a265508..3a3f50ac8a 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -14,7 +14,7 @@ open Tacmach open Decl_expr open Decl_mode open Pretyping.Default -open Rawterm +open Glob_term open Term open Pp open Compat @@ -343,13 +343,13 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in let pat_vars,aliases,patt = interp_pattern env pat in let inject = function - Thesis (Plain) -> Rawterm.GSort(dummy_loc,RProp Null) + Thesis (Plain) -> Glob_term.GSort(dummy_loc,RProp Null) | Thesis (For rec_occ) -> if not (List.mem rec_occ pat_vars) then errorlabstrm "suppose it is" (str "Variable " ++ Nameops.pr_id rec_occ ++ str " does not occur in pattern."); - Rawterm.GSort(dummy_loc,RProp Null) + Glob_term.GSort(dummy_loc,RProp Null) | This (c,_) -> c in let term1 = glob_constr_of_hyps inject hyps raw_prop in let loc_ids,npatt = |