diff options
| author | msozeau | 2008-06-21 17:10:28 +0000 |
|---|---|---|
| committer | msozeau | 2008-06-21 17:10:28 +0000 |
| commit | 8874a5916bc43acde325f67a73544a4beb65c781 (patch) | |
| tree | dc87ed564b07fd3901d33f3e570d42df501654f7 /interp/constrintern.ml | |
| parent | 15682aeca70802dba6f7e13b66521d4ab9e13af9 (diff) | |
Code cleanup in typeclasses, remove dead and duplicated code.
Change from named_context to rel_context for class params and fields.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11163 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 21 |
1 files changed, 2 insertions, 19 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ac4639b435..1ddcac276e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1275,23 +1275,6 @@ let intern_ltac isarity ltacvars sigma env c = type manual_implicits = (explicitation * (bool * bool)) list -let implicits_of_rawterm l = - let rec aux i c = - match c with - RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> - let rest = aux (succ i) b in - if bk = Implicit then - let name = - match na with - Name id -> Some id - | Anonymous -> None - in - (ExplByPos (i, name), (true, true)) :: rest - else rest - | RLetIn (loc, na, t, b) -> aux i b - | _ -> [] - in aux 1 l - (*********************************************************************) (* Functions to parse and interpret constructions *) @@ -1321,11 +1304,11 @@ let interp_constr_evars_gen_impls ?evdref match evdref with | None -> let c = intern_gen (kind=IsType) ~impls Evd.empty env c in - let imps = implicits_of_rawterm c in + let imps = Implicit_quantifiers.implicits_of_rawterm c in Default.understand_gen kind Evd.empty env c, imps | Some evdref -> let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in - let imps = implicits_of_rawterm c in + let imps = Implicit_quantifiers.implicits_of_rawterm c in Default.understand_tcc_evars evdref env kind c, imps let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c = |