diff options
| author | herbelin | 2006-01-09 22:00:34 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-09 22:00:34 +0000 |
| commit | 4d37bb49bbeb640661748edc90904d2f9b299a74 (patch) | |
| tree | 1455338e56818d030325b6d2571b8ec2bd115fe1 /interp | |
| parent | 865c375dc799b284e99f0408da80aed27553a55b (diff) | |
Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement dans Topconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7826 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 8 | ||||
| -rw-r--r-- | interp/topconstr.ml | 6 | ||||
| -rw-r--r-- | interp/topconstr.mli | 2 |
3 files changed, 9 insertions, 7 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8dc060d794..df641ecd04 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -698,18 +698,12 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Syntax extensions *) -let coerce_to_id = function - | CRef (Ident (_,id)) -> id - | c -> - user_err_loc (constr_loc c, "subst_rawconstr", - str"This expression should be a simple identifier") - let traverse_binder subst id (ids,tmpsc,scopes as env) = try (* Binders bound in the notation are consider first-order object *) (* and binders not bound in the notation do not capture variables *) (* outside the notation *) - let id' = coerce_to_id (fst (List.assoc id subst)) in + let _,id' = coerce_to_id (fst (List.assoc id subst)) in id', (Idset.add id' ids,tmpsc,scopes) with Not_found -> id, env diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 36a5426373..771c5716b2 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -630,6 +630,12 @@ let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b) let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b) let mkProdC (idl,a,b) = CProdN (dummy_loc,[idl,a],b) +let coerce_to_id = function + | CRef (Ident (loc,id)) -> (loc,id) + | a -> user_err_loc + (constr_loc a,"coerce_to_id", + str "This expression should be a simple identifier") + (* Used in correctness and interface *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 84342b2209..5b9d69cd67 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -142,6 +142,8 @@ val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr val mkLetInC : name located * constr_expr * constr_expr -> constr_expr val mkProdC : name located list * constr_expr * constr_expr -> constr_expr +val coerce_to_id : constr_expr -> identifier located + (* For binders parsing *) (* Includes let binders *) |