diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-07 08:43:02 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-07 08:43:02 +0000 |
| commit | 2ec0991f0fef6b529a0d90d64f06aff1c8db91ab (patch) | |
| tree | d27d471e35a635a8d783b496b557b30b75dd9784 /contrib | |
| parent | ad228a6815329a1331d26caca7f6eaae0ddbd52b (diff) | |
Two constants had been given in the wrong package (Logic_type instead of
the correct Logic_Type).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1554 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/pbp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index 7d3c4400c..a5f44847b 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -193,12 +193,12 @@ let prodconstr () = constant "Datatypes" "prod";; let exconstr () = constant "Logic" "ex";; let exTconstr () = constant "Logic_Type" "exT";; let sigconstr () = constant "Specif" "sig";; -let sigTconstr () = constant "Logic_type" "sigT";; +let sigTconstr () = constant "Logic_Type" "sigT";; let orconstr = Coqlib.build_coq_or;; let sumboolconstr = Coqlib.build_coq_sumbool;; let sumconstr() = constant "Datatypes" "sum";; let notconstr = Coqlib.build_coq_not;; -let notTconstr () = constant "Logic_type" "notT";; +let notTconstr () = constant "Logic_Type" "notT";; let is_matching_local a b = is_matching (pattern_of_constr a) b;; |