aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--contrib/interface/pbp.ml4
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;;