diff options
| author | msozeau | 2008-01-15 01:02:48 +0000 |
|---|---|---|
| committer | msozeau | 2008-01-15 01:02:48 +0000 |
| commit | 6cd832e28c48382cc9321825cc83db36f96ff8d5 (patch) | |
| tree | 51905b3dd36672bf17eeb6e82d45d26402800d7d /interp/constrextern.ml | |
| parent | d581efa789d7239b61d7c71f58fc980c350b2de1 (diff) | |
Generalize instance declarations to any context, better name handling. Add hole kind info for topconstrs.
Derive eta_expansion from functional extensionality axiom.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10439 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 06edeaed20..69d5ad67a9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -651,13 +651,13 @@ let rec extern inctx scopes vars r = | RVar (loc,id) -> CRef (Ident (loc,id)) - | REvar (loc,n,None) when !print_meta_as_hole -> CHole loc + | REvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None) | REvar (loc,n,l) -> extern_evar loc n (Option.map (List.map (extern false scopes vars)) l) | RPatVar (loc,n) -> - if !print_meta_as_hole then CHole loc else CPatVar (loc,n) + if !print_meta_as_hole then CHole (loc, None) else CPatVar (loc,n) | RApp (loc,f,args) -> (match f with @@ -756,7 +756,7 @@ let rec extern inctx scopes vars r = | RSort (loc,s) -> CSort (loc,extern_rawsort s) - | RHole (loc,e) -> CHole loc + | RHole (loc,e) -> CHole (loc, Some e) | RCast (loc,c, CastConv (k,t)) -> CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t)) |