diff options
| author | barras | 2003-09-22 18:09:11 +0000 |
|---|---|---|
| committer | barras | 2003-09-22 18:09:11 +0000 |
| commit | 66ee7ba58080fa8fcfdb4bb76b89cc0b70a8a4ac (patch) | |
| tree | e97e3bd30fa49fc5da4dfe207ff73e841ee083b1 /interp/constrextern.ml | |
| parent | fe027346f901f26d79ce243a06c08a8c9f661e81 (diff) | |
traducteur: affiche les commentaires a l'interieur des commandes
extraction: pb avec les variables de section definies
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e915c9ac62..b34ae524f2 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -548,17 +548,17 @@ let rec extern inctx scopes vars r = (f,args) in (match f with | REvar (loc,ev) -> extern_evar loc ev (* we drop args *) - | RRef (loc,ref) -> + | RRef (rloc,ref) -> let subscopes = Symbols.find_arguments_scope ref in let args = extern_args (extern true) (snd scopes) vars args subscopes in extern_app loc inctx (implicits_of_global_out ref) - (Some ref,extern_reference loc vars ref) + (Some ref,extern_reference rloc vars ref) args - | RVar (loc,id) -> (* useful for translation of inductive *) + | RVar (rloc,id) -> (* useful for translation of inductive *) let args = List.map (sub_extern true scopes vars) args in extern_app loc inctx (get_temporary_implicits_out id) - (None,Ident (loc,v7_to_v8_id id)) + (None,Ident (rloc,v7_to_v8_id id)) args | _ -> explicitize loc inctx [] (None,sub_extern false scopes vars f) |