diff options
| author | herbelin | 2000-05-03 18:04:46 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-03 18:04:46 +0000 |
| commit | 4c9696c6dac1beb1b19fe3bb083dee0b1ef1bd00 (patch) | |
| tree | 49317c7658ba1b6c95d0fbca122676288487f307 /parsing | |
| parent | 77f8b2363ac3e90587b93806e5780f4fff96ecc7 (diff) | |
suppression de Fw pour les implicites
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@405 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/astterm.ml | 2 | ||||
| -rw-r--r-- | parsing/pretty.ml | 4 | ||||
| -rw-r--r-- | parsing/termast.ml | 4 |
3 files changed, 5 insertions, 5 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 4bef9a0eb9..bdb0f17138 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -156,7 +156,7 @@ let dbize_ref k sigma env loc s = try match lookup_id id env with | RELNAME(n,_) -> RRef (loc,RVar id),[] - | _ -> RRef(loc,RVar id), (try implicits_of_var k id with _ -> []) + | _ -> RRef(loc,RVar id), (try implicits_of_var id with _ -> []) with Not_found -> try let c,il = match k with diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 19773d6869..641fa40356 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -223,7 +223,7 @@ let print_extracted_mutual sp = let print_variable sp = let (name,typ,_,_) = out_variable sp in - let l = implicits_of_var (kind_of_path sp) name in + let l = implicits_of_var name in [< print_var (string_of_id name) typ; print_impl_args l; 'fNL >] let print_constant with_values sep sp = @@ -453,7 +453,7 @@ let print_name name = | VAR _ -> let (_,typ) = Global.lookup_var name in [< print_var str typ; - try print_impl_args (implicits_of_var CCI name) + try print_impl_args (implicits_of_var name) with _ -> [<>] >] | DOPN(Const sp,_) -> print_constant true " = " sp diff --git a/parsing/termast.ml b/parsing/termast.ml index 183c015eae..ce180ba1c7 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -174,7 +174,7 @@ let implicit_of_ref = function | RConstruct (cstrid,_) -> constructor_implicits_list cstrid | RInd (indid,_) -> inductive_implicits_list indid | RConst (sp,_) -> constant_implicits_list sp - | RVar id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *) + | RVar id -> (try (implicits_of_var id) with _ -> []) (* et FW? *) | _ -> [] let rec skip_coercion dest_ref (f,args as app) = @@ -452,7 +452,7 @@ let bdize_app c al = | DOPN(MutConstruct constr_sp,_) -> constructor_implicits_list constr_sp | DOPN(MutInd ind_sp,_) -> inductive_implicits_list ind_sp | DOPN(Const sp,_) -> constant_implicits_list sp - | VAR id -> (try (implicits_of_var CCI id) with _ -> []) (* et FW? *) + | VAR id -> (try implicits_of_var id with _ -> []) (* et FW? *) | _ -> [] in if !print_implicits then |