diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-19 17:35:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-19 17:35:03 +0000 |
| commit | 1abd56dea147493178a582569f50c9c6f03c6008 (patch) | |
| tree | 940ad7cdc5bef6de02ea76d7b7bd450920313798 /pretyping/pretyping.ml | |
| parent | 4f17ea4dcc68bb4619dbf2b8578333288f145fe5 (diff) | |
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
Utilisation d'ident plutôt que int pour PMeta/CPatVar
Ajout CEvar pour la saisie des Evar
Pas d'entrée utilisateur pour les Meta noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e4714468a..f94c14e71 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -28,6 +28,7 @@ open Pretype_errors open Rawterm open Evarconv open Coercion +open Pattern open Dyn @@ -151,7 +152,13 @@ let evar_type_case isevars env ct pt lft p c = in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty) *) -let pretype_id loc env lvar id = +let strip_meta id = (* For Grammar v7 compatibility *) + let s = string_of_id id in + if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1)) + else id + +let pretype_id loc env lvar id = + let id = strip_meta id in (* May happen in tactics defined by Grammar *) try List.assoc id lvar with Not_found -> @@ -217,7 +224,8 @@ let rec pretype tycon env isevars lvar lmeta = function let j = (Retyping.get_judgment_of env (evars_of isevars) c) in inh_conv_coerce_to_tycon loc env isevars j tycon - | RMeta (loc,n) -> + | RPatVar (loc,(someta,n)) -> + assert (not someta); let j = try List.assoc n lmeta @@ -225,7 +233,7 @@ let rec pretype tycon env isevars lvar lmeta = function Not_found -> user_err_loc (loc,"pretype", - str "Metavariable " ++ int n ++ str " is unbound") + str "Metavariable " ++ pr_patvar n ++ str " is unbound") in inh_conv_coerce_to_tycon loc env isevars j tycon | RHole (loc,k) -> @@ -618,7 +626,7 @@ let ise_infer_type_gen fail_evar sigma env lvar lmeta c = check_evars fail_evar env sigma isevars tj.utj_val; (evars_of isevars, tj) -type meta_map = (int * unsafe_judgment) list +type meta_map = (patvar * unsafe_judgment) list type var_map = (identifier * unsafe_judgment) list let understand_judgment sigma env c = |