aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-29 16:02:05 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-29 16:02:05 +0000
commit4490dfcb94057dd6518963a904565e3a4a354bac (patch)
treec35cdb94182d5c6e9197ee131d9fe2ebf5a7d139 /plugins/cc
parenta188216d8570144524c031703860b63f0a53b56e (diff)
Splitting Term into five unrelated interfaces:
1. sorts.ml: A small file utility for sorts; 2. constr.ml: Really low-level terms, essentially kind_of_constr, smart constructor and basic operators; 3. vars.ml: Everything related to term variables, that is, occurences and substitution; 4. context.ml: Rel/Named context and all that; 5. term.ml: derived utility operations on terms; also includes constr.ml up to some renaming, and acts as a compatibility layer, to be deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml1
-rw-r--r--plugins/cc/cctac.ml3
2 files changed, 3 insertions, 1 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 473199cb2..aba908d48 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -15,6 +15,7 @@ open Pp
open Goptions
open Names
open Term
+open Vars
open Tacmach
open Evd
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index a5baa00f9..a7800667f 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -13,6 +13,7 @@ open Names
open Inductiveops
open Declarations
open Term
+open Vars
open Tacmach
open Tactics
open Tacticals
@@ -226,7 +227,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
let lp=Array.length types in
let ci=pred (snd cstr) in
let branch i=
- let ti=Term.prod_appvect types.(i) argv in
+ let ti= prod_appvect types.(i) argv in
let rc=fst (decompose_prod_assum ti) in
let head=
if i=ci then special else default in