diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-07 10:02:40 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-07 10:02:40 +0000 |
| commit | 78384438637eb9ce2f11f61bafc59f17c5f933da (patch) | |
| tree | f1968f737066e0e736f01b5fd4c8c9c5bccacdfc /toplevel | |
| parent | 9c662cf9e8f4065ab354dc9c55c3e819f0db1fbe (diff) | |
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/class.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 022c75cb6..e0ae40af6 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -60,7 +60,6 @@ let stre_of_coe = function | ConstRef sp -> constant_or_parameter_strength sp | VarRef sp -> variable_strength sp | IndRef _ | ConstructRef _ -> NeverDischarge - | EvarRef _ -> anomaly "Not a persistent reference" (* verfications pour l'ajout d'une classe *) @@ -197,9 +196,7 @@ let class_of_ref = function errorlabstrm "class_of_ref" [< 'sTR "Constructors, such as "; Printer.pr_global c; 'sTR " cannot be used as class" >] - | EvarRef _ -> - errorlabstrm "class_of_ref" - [< 'sTR "Existential variables cannot be used as class" >] + (* lp est la liste (inverse'e) des arguments de la coercion ids est le nom de la classe source @@ -479,4 +476,3 @@ let process_coercion sec_sp (((coe,coeinfo),s,t) as x) = (((ConstructRef ((newsp,i),j)),coeinfo),s1,t1) else ((coe,coeinfo),s1,t1) - | EvarRef _ -> anomaly "No Evar expected here as coercion" |